let OTS be OrdTrapSpace; :: thesis: for a, b, c, d being Element of
for a', b', c', d' being Element of st a = a' & b = b' & c = c' & d = d' holds
( a',b' // c',d' iff ( a,b // c,d or a,b // d,c ) )
let a, b, c, d be Element of ; :: thesis: for a', b', c', d' being Element of st a = a' & b = b' & c = c' & d = d' holds
( a',b' // c',d' iff ( a,b // c,d or a,b // d,c ) )
let a', b', c', d' be Element of ; :: thesis: ( a = a' & b = b' & c = c' & d = d' implies ( a',b' // c',d' iff ( a,b // c,d or a,b // d,c ) ) )
A1: Lambda OTS = AffinStruct(# the carrier of OTS,(lambda the CONGR of OTS) #) by DIRAF:def 2;
assume A2: ( a = a' & b = b' & c = c' & d = d' ) ; :: thesis: ( a',b' // c',d' iff ( a,b // c,d or a,b // d,c ) )

hereby :: thesis: ( ( a,b // c,d or a,b // d,c ) implies a',b' // c',d' )

assume a',b' // c',d' ; :: thesis: ( a,b // c,d or a,b // d,c )
then [[a',b'],[c',d']] in lambda the CONGR of OTS by A1, ANALOAF:def 2;
then ( [[a,b],[c,d]] in the CONGR of OTS or [[a,b],[d,c]] in the CONGR of OTS ) by A2, DIRAF:def 1;
hence ( a,b // c,d or a,b // d,c ) by ANALOAF:def 2; :: thesis: verum

end;

assume ( a,b // c,d or a,b // d,c ) ; :: thesis: a',b' // c',d'
then ( [[a,b],[c,d]] in the CONGR of OTS or [[a,b],[d,c]] in the CONGR of OTS ) by ANALOAF:def 2;
then [[a,b],[c,d]] in the CONGR of (Lambda OTS) by A1, DIRAF:def 1;
hence a',b' // c',d' by A2, ANALOAF:def 2; :: thesis: verum