Triangle has been worked on

source/Scrolls/TriangleScroll.mmt

@@ -18,6 +18,22 @@ theory TriangleScroll =
             ❘ meta ?MetaAnnotations?label "C"
             ❘ meta ?MetaAnnotations?description "The third point"
         ❙
+        // D: point
+            ❘ meta ?MetaAnnotations?label "D"
+            ❘ meta ?MetaAnnotations?description "The fourth point"
+        ❙
+        // dAB: Σ x:ℝ . ⊦ (d- A B) ≐ x
+         ❘ meta ?MetaAnnotations?label s"d${lverb A B}"
+         ❘ meta ?MetaAnnotations?description s"The distance from point ${lverb A} to point ${lverb B}"
+        ❙
+        // dDC: Σ x:ℝ . ⊦ (d- D C) ≐ x
+         ❘ meta ?MetaAnnotations?label s"d${lverb D C}"
+         ❘ meta ?MetaAnnotations?description s"The distance from point ${lverb D} to point ${lverb C}"
+        ❙
+        // rADC: ⊦ (∠ A,D,C) ≐ 90.0
+         ❘ meta ?MetaAnnotations?label s"r${lverb D}"
+         ❘ meta ?MetaAnnotations?description s"A right angle between ${lverb A D C}, where ${lverb D} is the point enclosed by ${lverb A} and ${lverb C}"
+        ❙
     ❚
 
     theory Solution =

source/Scrolls/TriangleType.mmt

@@ -7,4 +7,12 @@ theory TriangleType =
 
     triangleType : type ❘ # Triangle ❙
     triangleCons : point ⟶ point ⟶ point ⟶ Triangle ❘ # TriangleCons 1 2 3 ❙
+
+    // triangleA : triangle ⟶ point ❘ # triangleA 1 ❙
+    // triangleB : triangle ⟶ point ❘ # triangleB 1 ❙
+    // triangleC : triangle ⟶ point ❘ # triangleC 1 ❙
+
+    // axTriangleA : {a, b, c} ⊦ triangleA (triangleCons a b c) ≐ a  ❘ role Simplify ❙
+    // axTriangleB : {a, b, c} ⊦ triangleB (triangleCons a b c) ≐ b  ❘ role Simplify ❙
+    // axTriangleC : {a, b, c} ⊦ triangleC (triangleCons a b c) ≐ c  ❘ role Simplify ❙
 ❚
\ No newline at end of file