theorem :: GTARSKI3:119

for S being TarskiGeometryStruct holds
( S is satisfying_CongruenceEquivalenceRelation iff S is (TE) ) ;