let L1, L2 be non empty antisymmetric RelStr ; :: thesis: for D being non empty Subset of [:L1,L2:] st ( [:L1,L2:] is complete or ex_sup_of D,[:L1,L2:] ) holds
sup D = [(sup (proj1 D)),(sup (proj2 D))]
let D be non empty Subset of [:L1,L2:]; :: thesis: ( ( [:L1,L2:] is complete or ex_sup_of D,[:L1,L2:] ) implies sup D = [(sup (proj1 D)),(sup (proj2 D))] )
reconsider C1 = the carrier of L1, C2 = the carrier of L2 as non empty set ;
reconsider D' = D as non empty Subset of [:C1,C2:] by Def2;
not proj1 D' is empty ;
then reconsider D1 = proj1 D as non empty Subset of L1 ;
not proj2 D' is empty ;
then reconsider D2 = proj2 D as non empty Subset of L2 ;
assume ( [:L1,L2:] is complete or ex_sup_of D,[:L1,L2:] ) ; :: thesis: sup D = [(sup (proj1 D)),(sup (proj2 D))]
then A1: ex_sup_of D,[:L1,L2:] by YELLOW_0:17;
then A2: ( ex_sup_of D1,L1 & ex_sup_of D2,L2 ) by Th41;
then A3: ex_sup_of [:D1,D2:],[:L1,L2:] by Th39;
the carrier of [:L1,L2:] = [:C1,C2:] by Def2;
then consider d1, d2 being set such that
A4: ( d1 in C1 & d2 in C2 & sup D = [d1,d2] ) by ZFMISC_1:def 2;
reconsider d1 = d1 as Element of L1 by A4;
reconsider d2 = d2 as Element of L2 by A4;
A5: D1 is_<=_than d1

proof

let b be Element of L1; :: according to LATTICE3:def 9 :: thesis: ( not b in D1 or b <= d1 )
assume b in D1 ; :: thesis: b <= d1
then consider x being set such that
A6: [b,x] in D by RELAT_1:def 4;
reconsider x = x as Element of D2 by A6, FUNCT_5:4;
reconsider x = x as Element of L2 ;
D is_<=_than [d1,d2] by A1, A4, YELLOW_0:def 9;
then [b,x] <= [d1,d2] by A6, LATTICE3:def 9;
hence b <= d1 by Th11; :: thesis: verum

end;

D2 is_<=_than d2

proof

let b be Element of L2; :: according to LATTICE3:def 9 :: thesis: ( not b in D2 or b <= d2 )
assume b in D2 ; :: thesis: b <= d2
then consider x being set such that
A7: [x,b] in D by RELAT_1:def 5;
reconsider x = x as Element of D1 by A7, FUNCT_5:4;
reconsider x = x as Element of L1 ;
D is_<=_than [d1,d2] by A1, A4, YELLOW_0:def 9;
then [x,b] <= [d1,d2] by A7, LATTICE3:def 9;
hence b <= d2 by Th11; :: thesis: verum

end;

then ( sup D1 <= d1 & sup D2 <= d2 ) by A2, A5, YELLOW_0:def 9;
then A8: [(sup D1),(sup D2)] <= sup D by A4, Th11;
D' c= [:D1,D2:] by Th1;
then sup D <= sup [:D1,D2:] by A1, A3, YELLOW_0:34;
then sup D <= [(sup (proj1 D)),(sup (proj2 D))] by A2, Th43;
hence sup D = [(sup (proj1 D)),(sup (proj2 D))] by A8, ORDERS_2:25; :: thesis: verum