theorem :: GTARSKI3:120

for S being TarskiGeometryStruct holds
( S is satisfying_CongruenceIdentity iff S is (IE) ) ;