let OTS be OrdTrapSpace; :: thesis: for a, b, c, d being Element of OTS
for a', b', c', d' being Element of (Lambda OTS) 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 OTS; :: thesis: for a', b', c', d' being Element of (Lambda OTS) 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 (Lambda OTS); :: thesis: ( a = a' & b = b' & c = c' & d = d' implies ( a',b' // c',d' iff ( a,b // c,d or a,b // d,c ) ) )
assume A1:
( a = a' & b = b' & c = c' & d = d' )
; :: thesis: ( a',b' // c',d' iff ( a,b // c,d or a,b // d,c ) )
A2:
Lambda OTS = AffinStruct(# the carrier of OTS,(lambda the CONGR of OTS) #)
by DIRAF:def 2;
A3:
now 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 A2, ANALOAF:def 2;
then
(
[[a,b],[c,d]] in the
CONGR of
OTS or
[[a,b],[d,c]] in the
CONGR of
OTS )
by A1, DIRAF:def 1;
hence
(
a,
b // c,
d or
a,
b // d,
c )
by ANALOAF:def 2;
:: thesis: verum end;
now 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 A2, DIRAF:def 1;
hence
a',
b' // c',
d'
by A1, ANALOAF:def 2;
:: thesis: verum end;
hence
( a',b' // c',d' iff ( a,b // c,d or a,b // d,c ) )
by A3; :: thesis: verum