let S, T be non empty up-complete Poset; :: thesis: for a, c being Element of S
for b, d being Element of T holds
( [a,b] << [c,d] iff ( a << c & b << d ) )
let a, c be Element of S; :: thesis: for b, d being Element of T holds
( [a,b] << [c,d] iff ( a << c & b << d ) )
let b, d be Element of T; :: thesis: ( [a,b] << [c,d] iff ( a << c & b << d ) )
thus ( [a,b] << [c,d] implies ( a << c & b << d ) ) by Th18; :: thesis: ( a << c & b << d implies [a,b] << [c,d] )
assume A1: for D being non empty directed Subset of S st c <= sup D holds
ex e being Element of S st
( e in D & a <= e ) ; :: according to WAYBEL_3:def 1 :: thesis: ( not b << d or [a,b] << [c,d] )
assume A2: for D being non empty directed Subset of T st d <= sup D holds
ex e being Element of T st
( e in D & b <= e ) ; :: according to WAYBEL_3:def 1 :: thesis: [a,b] << [c,d]
let D be non empty directed Subset of [:S,T:]; :: according to WAYBEL_3:def 1 :: thesis: ( not [c,d] <= "\/" (D,[:S,T:]) or ex b₁ being M3( the carrier of [:S,T:]) st
( b₁ in D & [a,b] <= b₁ ) )
assume A3: [c,d] <= sup D ; :: thesis: ex b₁ being M3( the carrier of [:S,T:]) st
( b₁ in D & [a,b] <= b₁ )
ex_sup_of D,[:S,T:] by WAYBEL_0:75;
then A4: sup D = [(sup (proj1 D)),(sup (proj2 D))] by YELLOW_3:46;
then ( not proj1 D is empty & proj1 D is directed & c <= sup (proj1 D) ) by A3, YELLOW_3:11, YELLOW_3:21, YELLOW_3:22;
then consider e being Element of S such that
A5: e in proj1 D and
A6: a <= e by A1;
consider e2 being object such that
A7: [e,e2] in D by A5, XTUPLE_0:def 12;
( not proj2 D is empty & proj2 D is directed & d <= sup (proj2 D) ) by A3, A4, YELLOW_3:11, YELLOW_3:21, YELLOW_3:22;
then consider f being Element of T such that
A8: f in proj2 D and
A9: b <= f by A2;
consider f1 being object such that
A10: [f1,f] in D by A8, XTUPLE_0:def 13;
A11: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def 2;
then reconsider e2 = e2 as Element of T by A7, ZFMISC_1:87;
reconsider f1 = f1 as Element of S by A11, A10, ZFMISC_1:87;
consider ef being Element of [:S,T:] such that
A12: ef in D and
A13: ( [e,e2] <= ef & [f1,f] <= ef ) by A7, A10, WAYBEL_0:def 1;
A14: ef = [(ef `1),(ef `2)] by A11, MCART_1:21;
then ( e <= ef `1 & f <= ef `2 ) by A13, YELLOW_3:11;
then A15: [e,f] <= ef by A14, YELLOW_3:11;
take ef ; :: thesis: ( ef in D & [a,b] <= ef )
thus ef in D by A12; :: thesis: [a,b] <= ef
[a,b] <= [e,f] by A6, A9, YELLOW_3:11;
hence [a,b] <= ef by A15, ORDERS_2:3; :: thesis: verum