theorem :: GTARSKI3:124

for S being TarskiGeometryStruct holds
( S is satisfying_Lower_Dimension_Axiom iff S is (Lo2) ) ;