let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct ; :: thesis: ( S is satisfying_SAS iff S is (FS) )
hereby :: thesis: ( S is (FS) implies S is satisfying_SAS )
assume S is satisfying_SAS ; :: thesis: S is (FS)
then S is satisfying_SST_A5 ;
hence S is (FS) ; :: thesis: verum
end;
assume S is (FS) ; :: thesis: S is satisfying_SAS
then S is satisfying_SST_A5 ;
hence S is satisfying_SAS ; :: thesis: verum