let OTS be OrdTrapSpace; :: thesis: for a, b, c, d being Element of OTS
for a9, b9, c9, d9 being Element of (Lambda OTS) st a = a9 & b = b9 & c = c9 & d = d9 holds
( a9,b9 // c9,d9 iff ( a,b // c,d or a,b // d,c ) )
let a, b, c, d be Element of OTS; :: thesis: for a9, b9, c9, d9 being Element of (Lambda OTS) st a = a9 & b = b9 & c = c9 & d = d9 holds
( a9,b9 // c9,d9 iff ( a,b // c,d or a,b // d,c ) )
let a9, b9, c9, d9 be Element of (Lambda OTS); :: thesis: ( a = a9 & b = b9 & c = c9 & d = d9 implies ( a9,b9 // c9,d9 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 = a9 & b = b9 & c = c9 & d = d9 ) ; :: thesis: ( a9,b9 // c9,d9 iff ( a,b // c,d or a,b // d,c ) )

hereby :: thesis: ( ( a,b // c,d or a,b // d,c ) implies a9,b9 // c9,d9 )

assume a9,b9 // c9,d9 ; :: thesis: ( a,b // c,d or a,b // d,c )
then [[a9,b9],[c9,d9]] 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: a9,b9 // c9,d9
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 a9,b9 // c9,d9 by A2, ANALOAF:def 2; :: thesis: verum