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