diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt index 98311f40f85043eef2d85c1b8f233da80eb2a3da..b4a01226e2ad74e2f83aae5953dd2a6fa0c6a5a0 100644 --- a/source/MetaTheories.mmt +++ b/source/MetaTheories.mmt @@ -377,6 +377,7 @@ theory PyramidType = include ☞http://mathhub.info/MitM/core/geometry?3DGeometry â™ include ☞http://mathhub.info/MitM/core/geometry?Planes â™ include ?FrameITBasics â™ + include ?RectangleType â™ pyramidType : type ☠# Pyramid â™ pyramidCons : Rectangle ⟶ point ⟶ Pyramid ☠# PyramidCons 1 2 â™