let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct ; :: thesis: ( S is satisfying_SAS iff S is satisfying_SST_A5 )
thus ( S is satisfying_SAS implies S is satisfying_SST_A5 ) :: thesis: ( S is satisfying_SST_A5 implies S is satisfying_SAS )
proof
assume A1: S is satisfying_SAS ; :: thesis: S is satisfying_SST_A5
now :: thesis: for a, b, c, d, a9, b9, c9, d9 being POINT of S st a <> b & between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 & a,d equiv a9,d9 & b,d equiv b9,d9 holds
c,d equiv c9,d9
let a, b, c, d, a9, b9, c9, d9 be POINT of S; :: thesis: ( a <> b & between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 & a,d equiv a9,d9 & b,d equiv b9,d9 implies c,d equiv c9,d9 )
assume A2: ( a <> b & between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 & a,d equiv a9,d9 & b,d equiv b9,d9 ) ; :: thesis: c,d equiv c9,d9
then a,b,d cong a9,b9,d9 ;
then d,c equiv d9,c9 by A1, A2;
then c,d equiv d9,c9 by Satz2p4;
hence c,d equiv c9,d9 by Satz2p5; :: thesis: verum
end;
hence S is satisfying_SST_A5 ; :: thesis: verum
end;
thus ( S is satisfying_SST_A5 implies S is satisfying_SAS ) :: thesis: verum
proof
assume A3: S is satisfying_SST_A5 ; :: thesis: S is satisfying_SAS
now :: thesis: for a, b, c, x, a1, b1, c1, x1 being POINT of S st a <> b & a,b,c cong a1,b1,c1 & between a,b,x & between a1,b1,x1 & b,x equiv b1,x1 holds
c,x equiv c1,x1
let a, b, c, x, a1, b1, c1, x1 be POINT of S; :: thesis: ( a <> b & a,b,c cong a1,b1,c1 & between a,b,x & between a1,b1,x1 & b,x equiv b1,x1 implies c,x equiv c1,x1 )
assume ( a <> b & a,b,c cong a1,b1,c1 & between a,b,x & between a1,b1,x1 & b,x equiv b1,x1 ) ; :: thesis: c,x equiv c1,x1
then x,c equiv x1,c1 by A3;
then c,x equiv x1,c1 by Satz2p4;
hence c,x equiv c1,x1 by Satz2p5; :: thesis: verum
end;
hence S is satisfying_SAS ; :: thesis: verum
end;