let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity TarskiGeometryStruct ; :: thesis: for a, b, c, d being POINT of S st a,b equiv c,d 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 c1, c2, c3, c4 be POINT of S; :: thesis: ( c1,c2 equiv c3,c4 implies ( c1,c2 equiv c4,c3 & c2,c1 equiv c3,c4 & c2,c1 equiv c4,c3 & c3,c4 equiv c1,c2 & c4,c3 equiv c1,c2 & c3,c4 equiv c2,c1 & c4,c3 equiv c2,c1 ) )
assume A1: c1,c2 equiv c3,c4 ; :: thesis: ( c1,c2 equiv c4,c3 & c2,c1 equiv c3,c4 & c2,c1 equiv c4,c3 & c3,c4 equiv c1,c2 & c4,c3 equiv c1,c2 & c3,c4 equiv c2,c1 & c4,c3 equiv c2,c1 )
assume A2: ( not c1,c2 equiv c4,c3 or not c2,c1 equiv c3,c4 or not c2,c1 equiv c4,c3 or not c3,c4 equiv c1,c2 or not c4,c3 equiv c1,c2 or not c3,c4 equiv c2,c1 or not c4,c3 equiv c2,c1 ) ; :: thesis: contradiction
A3: c1,c2 equiv c2,c1 by GTARSKI1:def 5;
then A4: c3,c4 equiv c2,c1 by A1, GTARSKI1:def 6;
c1,c2 equiv c1,c2 by GTARSKI3:1;
then A5: c3,c4 equiv c1,c2 by A1, GTARSKI1:def 6;
c3,c4 equiv c4,c3 by GTARSKI1:def 5;
hence contradiction by A1, A2, A3, A4, A5, GTARSKI1:def 6; :: thesis: verum