let S1, S2 be non empty antisymmetric RelStr ; :: thesis: for D being Subset of [:S1,S2:] holds
( ( ex_inf_of proj1 D,S1 & ex_inf_of proj2 D,S2 ) iff ex_inf_of D,[:S1,S2:] )
let D be Subset of [:S1,S2:]; :: thesis: ( ( ex_inf_of proj1 D,S1 & ex_inf_of proj2 D,S2 ) iff ex_inf_of D,[:S1,S2:] )
A1: the carrier of [:S1,S2:] = [: the carrier of S1, the carrier of S2:] by Def2;
then A2: D c= [:(proj1 D),(proj2 D):] by Th1;

hereby :: thesis: ( ex_inf_of D,[:S1,S2:] implies ( ex_inf_of proj1 D,S1 & ex_inf_of proj2 D,S2 ) )

assume that
A3: ex_inf_of proj1 D,S1 and
A4: ex_inf_of proj2 D,S2 ; :: thesis: ex_inf_of D,[:S1,S2:]
ex a being Element of [:S1,S2:] st
( D is_>=_than a & ( for b being Element of [:S1,S2:] st D is_>=_than b holds
a >= b ) )

proof

consider x2 being Element of S2 such that
A5: proj2 D is_>=_than x2 and
A6: for b being Element of S2 st proj2 D is_>=_than b holds
x2 >= b by A4, YELLOW_0:16;
consider x1 being Element of S1 such that
A7: proj1 D is_>=_than x1 and
A8: for b being Element of S1 st proj1 D is_>=_than b holds
x1 >= b by A3, YELLOW_0:16;
take a = [x1,x2]; :: thesis: ( D is_>=_than a & ( for b being Element of [:S1,S2:] st D is_>=_than b holds
a >= b ) )
thus D is_>=_than a :: thesis: for b being Element of [:S1,S2:] st D is_>=_than b holds
a >= b

proof

let q be Element of [:S1,S2:]; :: according to LATTICE3:def 8 :: thesis: ( not q in D or a <= q )
assume q in D ; :: thesis: a <= q
then consider q1, q2 being object such that
A9: q1 in proj1 D and
A10: q2 in proj2 D and
A11: q = [q1,q2] by A2, ZFMISC_1:def 2;
reconsider q2 = q2 as Element of S2 by A10;
reconsider q1 = q1 as Element of S1 by A9;
( q1 >= x1 & q2 >= x2 ) by A7, A5, A9, A10;
hence a <= q by A11, Th11; :: thesis: verum

end;

let b be Element of [:S1,S2:]; :: thesis: ( D is_>=_than b implies a >= b )
assume A12: D is_>=_than b ; :: thesis: a >= b
A13: b = [(b `1),(b `2)] by A1, MCART_1:21;
then proj2 D is_>=_than b `2 by A12, Th34;
then A14: x2 >= b `2 by A6;
proj1 D is_>=_than b `1 by A12, A13, Th34;
then x1 >= b `1 by A8;
hence a >= b by A13, A14, Th11; :: thesis: verum

end;

hence ex_inf_of D,[:S1,S2:] by YELLOW_0:16; :: thesis: verum

end;

assume ex_inf_of D,[:S1,S2:] ; :: thesis: ( ex_inf_of proj1 D,S1 & ex_inf_of proj2 D,S2 )
then consider x being Element of [:S1,S2:] such that
A15: D is_>=_than x and
A16: for b being Element of [:S1,S2:] st D is_>=_than b holds
x >= b by YELLOW_0:16;
A17: x = [(x `1),(x `2)] by A1, MCART_1:21;
then A18: proj1 D is_>=_than x `1 by A15, Th34;
A19: proj2 D is_>=_than x `2 by A15, A17, Th34;
for b being Element of S1 st proj1 D is_>=_than b holds
x `1 >= b

proof

let b be Element of S1; :: thesis: ( proj1 D is_>=_than b implies x `1 >= b )
assume proj1 D is_>=_than b ; :: thesis: x `1 >= b
then D is_>=_than [b,(x `2)] by A19, Th34;
then x >= [b,(x `2)] by A16;
hence x `1 >= b by A17, Th11; :: thesis: verum

end;

hence ex_inf_of proj1 D,S1 by A18, YELLOW_0:16; :: thesis: ex_inf_of proj2 D,S2
for b being Element of S2 st proj2 D is_>=_than b holds
x `2 >= b

proof

let b be Element of S2; :: thesis: ( proj2 D is_>=_than b implies x `2 >= b )
assume proj2 D is_>=_than b ; :: thesis: x `2 >= b
then D is_>=_than [(x `1),b] by A18, Th34;
then x >= [(x `1),b] by A16;
hence x `2 >= b by A17, Th11; :: thesis: verum

end;

hence ex_inf_of proj2 D,S2 by A19, YELLOW_0:16; :: thesis: verum