Changed Rectangle and Cuboid Fact

source/Scrolls/CuboidScroll.mmt

@@ -10,6 +10,7 @@ theory CuboidScroll =
     meta ?MetaAnnotations?problemTheory  ?CuboidScroll/Problem ❙
     meta ?MetaAnnotations?solutionTheory ?CuboidScroll/Solution ❙
     theory Problem =
+
         R: Rectangle
          ❘ meta ?MetaAnnotations?label "R"
          ❘ meta ?MetaAnnotations?description "The given rectangle"
@@ -19,20 +20,6 @@ theory CuboidScroll =
          ❘ meta ?MetaAnnotations?description "The point above the centerpoint of the rectangle"
         ❙
 
-        rTBA: ⊦ (∠ T,(R _getB),(R _getA)) ≐ 90.0
-         ❘ meta ?MetaAnnotations?label "rTBA"
-         ❘ meta ?MetaAnnotations?description "A right angle between TBA, where B is the point enclosed by T and A"
-        ❙
-
-        rTBC: ⊦ (∠ T,(R _getB),(R _getC)) ≐ 90.0
-         ❘ meta ?MetaAnnotations?label "rTBC"
-         ❘ meta ?MetaAnnotations?description "A right angle between TBC, where B is the point enclosed by T and C"
-        ❙
-
-
-
-
-    ❙
         
     ❚
     theory Solution =
@@ -41,7 +28,7 @@ theory CuboidScroll =
         meta ?MetaAnnotations?description s"Given a rectangle and a top point that lies above the point in the center of the right-angle formed by the squarepoints
                                             this scroll constructs a cuboid. Additionally you need a proof that there are two right angles between TBC and TBA" ❙
         ConstructedCuboid : Cuboid
-                ❘ = CuboidCons R T
+                ❘ = ( CuboidCons R T )
                 ❘ meta ?MetaAnnotations?label s"Cuboid"
                 ❘ meta ?MetaAnnotations?description s"The constructed Cuboid."
         ❙

source/Scrolls/CuboidType.mmt

@@ -2,11 +2,10 @@ namespace http://mathhub.info/FrameIT/frameworld ❚
 fixmeta ur:?LF ❚
 
 theory CuboidType =
-  
-  include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
-  include ?FrameITBasics ❙
+    include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
+    include ?FrameITBasics ❙
+    include ?RectangleType ❙
 
-  cuboidType : type ❘ # Cuboid ❙
-  cuboidCons : Rectangle ⟶ point  ⟶ Cuboid  ❘ # CuboidCons 1 2 ❙
-  
+    cuboidType : type ❘ # Cuboid ❙
+    cuboidCons : Rectangle ⟶ point ⟶ Cuboid ❘ # CuboidCons 1 2 ❙
 ❚
\ No newline at end of file

source/Scrolls/RectangleScroll.mmt

@@ -39,7 +39,6 @@ theory RectangleScroll =
         ❙
 
 
-    ❙
         
     ❚
     theory Solution =

source/Scrolls/RectangleType.mmt

@@ -9,11 +9,4 @@ theory RectangleType =
   rectangleType : type ❘ # Rectangle ❙
   rectangleCons : point ⟶ point ⟶ point  ⟶ Rectangle  ❘ # RectangleCons 1 2 3 ❙
   
-  getA : Rectangle ⟶ point ❘ # 1 _getA ❙
-  getB : Rectangle ⟶ point ❘ # 1 _getB ❙
-  getC : Rectangle ⟶ point ❘ # 1 _getC ❙
-
-  axiomgetA : {R: Rectangle} ⊦ (RectangleCons A B C) ≐ A ❙
-  axiomgetB : {R: Rectangle} ⊦ (RectangleCons A B C) ≐ B ❙
-  axiomgetC : {R: Rectangle} ⊦ (RectangleCons A B C) ≐ C ❙
 ❚
\ No newline at end of file