let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SAS TarskiGeometryStruct ; :: thesis: for a, b, c, d, a9, b9, c9, d9 being POINT of S st a,b,c,d AFS a9,b9,c9,d9 & a <> b holds
c,d equiv c9,d9
let a, b, c, d, a9, b9, c9, d9 be POINT of S; :: thesis: ( a,b,c,d AFS a9,b9,c9,d9 & a <> b implies c,d equiv c9,d9 )
assume A1: ( a,b,c,d AFS a9,b9,c9,d9 & a <> b ) ; :: thesis: c,d equiv c9,d9
S is satisfying_SST_A5 ;
hence c,d equiv c9,d9 by A1; :: thesis: verum