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