theorem EQUIV1: :: GTARSKI3:9

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