let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity TarskiGeometryStruct ; :: thesis: for p, q, a, b, c, d being POINT of S st ( p,q equiv a,b or p,q equiv b,a or q,p equiv a,b or q,p equiv b,a ) & ( p,q equiv c,d or p,q equiv d,c or q,p equiv c,d or q,p equiv d,c ) holds
( a,b equiv d,c & b,a equiv c,d & b,a equiv d,c & c,d equiv a,b & d,c equiv a,b & c,d equiv b,a & d,c equiv b,a )
let p, q, a, b, c, d be POINT of S; :: thesis: ( ( p,q equiv a,b or p,q equiv b,a or q,p equiv a,b or q,p equiv b,a ) & ( p,q equiv c,d or p,q equiv d,c or q,p equiv c,d or q,p equiv d,c ) implies ( a,b equiv d,c & b,a equiv c,d & b,a equiv d,c & c,d equiv a,b & d,c equiv a,b & c,d equiv b,a & d,c equiv b,a ) )
assume ( ( p,q equiv a,b or p,q equiv b,a or q,p equiv a,b or q,p equiv b,a ) & ( p,q equiv c,d or p,q equiv d,c or q,p equiv c,d or q,p equiv d,c ) ) ; :: thesis: ( a,b equiv d,c & b,a equiv c,d & b,a equiv d,c & c,d equiv a,b & d,c equiv a,b & c,d equiv b,a & d,c equiv b,a )
then ( p,q equiv a,b & p,q equiv c,d ) by Prelim01;
then a,b equiv c,d by GTARSKI1:def 6;
hence ( a,b equiv d,c & b,a equiv c,d & b,a equiv d,c & c,d equiv a,b & d,c equiv a,b & c,d equiv b,a & d,c equiv b,a ) by Prelim01; :: thesis: verum