let OTS be OrdTrapSpace; 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; 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); ( 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 )
; ( a9,b9 // c9,d9 iff ( a,b // c,d or a,b // d,c ) )
hereby ( ( a,b // c,d or a,b // d,c ) implies a9,b9 // c9,d9 )
assume
a9,
b9 // c9,
d9
;
( 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;
verum
end;
assume
( a,b // c,d or a,b // d,c )
; 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; verum