theorem :: GTARSKI3:118

for S being TarskiGeometryStruct holds
( S is satisfying_CongruenceSymmetry iff S is (RE) ) ;