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_inf_of D,[:L1,L2:] ) holds
inf D = [(inf (proj1 D)),(inf (proj2 D))]
let D be non empty Subset of [:L1,L2:]; :: thesis: ( ( [:L1,L2:] is complete or ex_inf_of D,[:L1,L2:] ) implies inf D = [(inf (proj1 D)),(inf (proj2 D))] )
reconsider C1 = the carrier of L1, C2 = the carrier of L2 as non empty set ;
the carrier of [:L1,L2:] = [:C1,C2:] by Def2;
then consider d1, d2 being object such that
A1: d1 in C1 and
A2: d2 in C2 and
A3: inf D = [d1,d2] by ZFMISC_1:def 2;
reconsider d1 = d1 as Element of L1 by A1;
reconsider D9 = D as non empty Subset of [:C1,C2:] by Def2;
not proj1 D9 is empty ;
then reconsider D1 = proj1 D as non empty Subset of L1 ;
not proj2 D9 is empty ;
then reconsider D2 = proj2 D as non empty Subset of L2 ;
A4: D9 c= [:D1,D2:] by Th1;
reconsider d2 = d2 as Element of L2 by A2;
assume ( [:L1,L2:] is complete or ex_inf_of D,[:L1,L2:] ) ; :: thesis: inf D = [(inf (proj1 D)),(inf (proj2 D))]
then A5: ex_inf_of D,[:L1,L2:] by YELLOW_0:17;
then A6: ex_inf_of D2,L2 by Th42;
A7: ex_inf_of D1,L1 by A5, Th42;
then ex_inf_of [:D1,D2:],[:L1,L2:] by A6, Th40;
then inf D >= inf [:D1,D2:] by A5, A4, YELLOW_0:35;
then A8: inf D >= [(inf (proj1 D)),(inf (proj2 D))] by A7, A6, Th44;
D2 is_>=_than d2

proof

let b be Element of L2; :: according to LATTICE3:def 8 :: thesis: ( not b in D2 or d2 <= b )
assume b in D2 ; :: thesis: d2 <= b
then consider x being object such that
A9: [x,b] in D by XTUPLE_0:def 13;
reconsider x = x as Element of D1 by A9, XTUPLE_0:def 12;
reconsider x = x as Element of L1 ;
D is_>=_than [d1,d2] by A5, A3, YELLOW_0:def 10;
then [x,b] >= [d1,d2] by A9;
hence d2 <= b by Th11; :: thesis: verum

end;

then A10: inf D2 >= d2 by A6, YELLOW_0:def 10;
D1 is_>=_than d1

proof

let b be Element of L1; :: according to LATTICE3:def 8 :: thesis: ( not b in D1 or d1 <= b )
assume b in D1 ; :: thesis: d1 <= b
then consider x being object such that
A11: [b,x] in D by XTUPLE_0:def 12;
reconsider x = x as Element of D2 by A11, XTUPLE_0:def 13;
reconsider x = x as Element of L2 ;
D is_>=_than [d1,d2] by A5, A3, YELLOW_0:def 10;
then [b,x] >= [d1,d2] by A11;
hence d1 <= b by Th11; :: thesis: verum

end;

then inf D1 >= d1 by A7, YELLOW_0:def 10;
then [(inf D1),(inf D2)] >= inf D by A3, A10, Th11;
hence inf D = [(inf (proj1 D)),(inf (proj2 D))] by A8, ORDERS_2:2; :: thesis: verum