theorem :: GTARSKI3:125

for S being TarskiGeometryStruct holds
( S is satisfying_Upper_Dimension_Axiom iff S is (Up2) ) ;