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 x1 being Element of S1 such that
A5: proj1 D is_>=_than x1 and
A6: for b being Element of S1 st proj1 D is_>=_than b holds
x1 >= b by A3, YELLOW_0:16;
consider x2 being Element of S2 such that
A7: proj2 D is_>=_than x2 and
A8: for b being Element of S2 st proj2 D is_>=_than b holds
x2 >= b by A4, 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 set such that
A9: ( q1 in proj1 D & q2 in proj2 D & q = [q1,q2] ) by A2, ZFMISC_1:def 2;
reconsider q1 = q1 as Element of S1 by A9;
reconsider q2 = q2 as Element of S2 by A9;
( q1 >= x1 & q2 >= x2 ) by A5, A7, A9, LATTICE3:def 8;
hence a <= q by A9, Th11; :: thesis: verum

end;

let b be Element of [:S1,S2:]; :: thesis: ( D is_>=_than b implies a >= b )
assume A10: D is_>=_than b ; :: thesis: a >= b
A11: b = [(b `1 ),(b `2 )] by A1, MCART_1:23;
then ( proj1 D is_>=_than b `1 & proj2 D is_>=_than b `2 ) by A10, Th34;
then ( x1 >= b `1 & x2 >= b `2 ) by A6, A8;
hence a >= b by A11, 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
A12: D is_>=_than x and
A13: for b being Element of [:S1,S2:] st D is_>=_than b holds
x >= b by YELLOW_0:16;
A14: x = [(x `1 ),(x `2 )] by A1, MCART_1:23;
then A15: proj1 D is_>=_than x `1 by A12, Th34;
A16: proj2 D is_>=_than x `2 by A12, A14, 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 A16, Th34;
then x >= [b,(x `2 )] by A13;
hence x `1 >= b by A14, Th11; :: thesis: verum

end;

hence ex_inf_of proj1 D,S1 by A15, 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 A15, Th34;
then x >= [(x `1 ),b] by A13;
hence x `2 >= b by A14, Th11; :: thesis: verum

end;

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