let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity TarskiGeometryStruct ; 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 or a,b equiv p,q or b,a equiv p,q or a,b equiv q,p or b,a equiv q,p ) & ( p,q equiv c,d or p,q equiv d,c or q,p equiv c,d or q,p equiv d,c or c,d equiv p,q or d,c equiv p,q or c,d equiv q,p or d,c equiv q,p ) 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 & a,b equiv c,d )
let p, q, a, b, c, d be POINT of S; ( ( p,q equiv a,b or p,q equiv b,a or q,p equiv a,b or q,p equiv b,a or a,b equiv p,q or b,a equiv p,q or a,b equiv q,p or b,a equiv q,p ) & ( p,q equiv c,d or p,q equiv d,c or q,p equiv c,d or q,p equiv d,c or c,d equiv p,q or d,c equiv p,q or c,d equiv q,p or d,c equiv q,p ) 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 & a,b equiv c,d ) )
assume
( ( p,q equiv a,b or p,q equiv b,a or q,p equiv a,b or q,p equiv b,a or a,b equiv p,q or b,a equiv p,q or a,b equiv q,p or b,a equiv q,p ) & ( p,q equiv c,d or p,q equiv d,c or q,p equiv c,d or q,p equiv d,c or c,d equiv p,q or d,c equiv p,q or c,d equiv q,p or d,c equiv q,p ) )
; ( 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 & a,b equiv c,d )
then
( p,q equiv a,b & p,q equiv c,d )
by Prelim01;
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 & a,b equiv c,d )
by Prelim02; verum