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] )
A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2;
assume A2: 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 A3: 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 M2(the carrier of [:S,T:]) st
( b₁ in D & [a,b] <= b₁ ) )
assume A4: [c,d] <= sup D ; :: thesis: ex b₁ being M2(the carrier of [:S,T:]) st
( b₁ in D & [a,b] <= b₁ )
A5: ( not proj1 D is empty & proj1 D is directed & not proj2 D is empty & proj2 D is directed ) by YELLOW_3:21, YELLOW_3:22;
ex_sup_of D,[:S,T:] by WAYBEL_0:75;
then A6: sup D = [(sup (proj1 D)),(sup (proj2 D))] by YELLOW_3:46;
then c <= sup (proj1 D) by A4, YELLOW_3:11;
then consider e being Element of S such that
A7: ( e in proj1 D & a <= e ) by A2, A5;
d <= sup (proj2 D) by A4, A6, YELLOW_3:11;
then consider f being Element of T such that
A8: ( f in proj2 D & b <= f ) by A3, A5;
consider e2 being set such that
A9: [e,e2] in D by A7, RELAT_1:def 4;
consider f1 being set such that
A10: [f1,f] in D by A8, RELAT_1:def 5;
reconsider e2 = e2 as Element of T by A1, A9, ZFMISC_1:106;
reconsider f1 = f1 as Element of S by A1, A10, ZFMISC_1:106;
consider ef being Element of [:S,T:] such that
A11: ( ef in D & [e,e2] <= ef & [f1,f] <= ef ) by A9, A10, WAYBEL_0:def 1;
take ef ; :: thesis: ( ef in D & [a,b] <= ef )
thus ef in D by A11; :: thesis: [a,b] <= ef
A12: [a,b] <= [e,f] by A7, A8, YELLOW_3:11;
A13: ef = [(ef `1 ),(ef `2 )] by A1, MCART_1:23;
then ( e <= ef `1 & f <= ef `2 ) by A11, YELLOW_3:11;
then [e,f] <= ef by A13, YELLOW_3:11;
hence [a,b] <= ef by A12, ORDERS_2:26; :: thesis: verum