let S1, S2 be non empty antisymmetric RelStr ; :: thesis: for D being Subset of [:S1,S2:] holds
( ( ex_sup_of proj1 D,S1 & ex_sup_of proj2 D,S2 ) iff ex_sup_of D,[:S1,S2:] )
let D be Subset of [:S1,S2:]; :: thesis: ( ( ex_sup_of proj1 D,S1 & ex_sup_of proj2 D,S2 ) iff ex_sup_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_sup_of D,[:S1,S2:] implies ( ex_sup_of proj1 D,S1 & ex_sup_of proj2 D,S2 ) )

assume that
A3: ex_sup_of proj1 D,S1 and
A4: ex_sup_of proj2 D,S2 ; :: thesis: ex_sup_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:15;
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:15;
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 9 :: thesis: ( not q in D or q <= a )
assume q in D ; :: thesis: q <= a
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 9;
hence q <= a 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, Th31;
then ( x1 <= b `1 & x2 <= b `2 ) by A6, A8;
hence a <= b by A11, Th11; :: thesis: verum

end;

hence ex_sup_of D,[:S1,S2:] by YELLOW_0:15; :: thesis: verum

end;

assume ex_sup_of D,[:S1,S2:] ; :: thesis: ( ex_sup_of proj1 D,S1 & ex_sup_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:15;
A14: x = [(x `1 ),(x `2 )] by A1, MCART_1:23;
then A15: proj1 D is_<=_than x `1 by A12, Th31;
A16: proj2 D is_<=_than x `2 by A12, A14, Th31;
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, Th31;
then x <= [b,(x `2 )] by A13;
hence x `1 <= b by A14, Th11; :: thesis: verum

end;

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

end;

hence ex_sup_of proj2 D,S2 by A16, YELLOW_0:15; :: thesis: verum