theorem :: GTARSKI3:127

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct holds
( S is satisfying_SAS iff S is (FS) )