theorem :: GTARSKI3:121

for S being TarskiGeometryStruct holds
( S is satisfying_SegmentConstruction iff S is (SC) ) ;