let S1, S2 be non empty antisymmetric RelStr ; :: thesis: for D1 being non empty Subset of S1
for D2 being non empty Subset of S2 holds
( ( ex_sup_of D1,S1 & ex_sup_of D2,S2 ) iff ex_sup_of [:D1,D2:],[:S1,S2:] )
let D1 be non empty Subset of S1; :: thesis: for D2 being non empty Subset of S2 holds
( ( ex_sup_of D1,S1 & ex_sup_of D2,S2 ) iff ex_sup_of [:D1,D2:],[:S1,S2:] )
let D2 be non empty Subset of S2; :: thesis: ( ( ex_sup_of D1,S1 & ex_sup_of D2,S2 ) iff ex_sup_of [:D1,D2:],[:S1,S2:] )

hereby :: thesis: ( ex_sup_of [:D1,D2:],[:S1,S2:] implies ( ex_sup_of D1,S1 & ex_sup_of D2,S2 ) )

assume that
A1: ex_sup_of D1,S1 and
A2: ex_sup_of D2,S2 ; :: thesis: ex_sup_of [:D1,D2:],[:S1,S2:]
consider a2 being Element of S2 such that
A3: D2 is_<=_than a2 and
A4: for b being Element of S2 st D2 is_<=_than b holds
a2 <= b by A2, YELLOW_0:15;
consider a1 being Element of S1 such that
A5: D1 is_<=_than a1 and
A6: for b being Element of S1 st D1 is_<=_than b holds
a1 <= b by A1, YELLOW_0:15;
ex a being Element of [:S1,S2:] st
( [:D1,D2:] is_<=_than a & ( for b being Element of [:S1,S2:] st [:D1,D2:] is_<=_than b holds
a <= b ) )

proof

take a = [a1,a2]; :: thesis: ( [:D1,D2:] is_<=_than a & ( for b being Element of [:S1,S2:] st [:D1,D2:] is_<=_than b holds
a <= b ) )
thus [:D1,D2:] is_<=_than a by A5, A3, Th30; :: thesis: for b being Element of [:S1,S2:] st [:D1,D2:] is_<=_than b holds
a <= b
let b be Element of [:S1,S2:]; :: thesis: ( [:D1,D2:] is_<=_than b implies a <= b )
assume A7: [:D1,D2:] is_<=_than b ; :: thesis: a <= b
the carrier of [:S1,S2:] = [: the carrier of S1, the carrier of S2:] by Def2;
then A8: b = [(b `1),(b `2)] by MCART_1:21;
then D2 is_<=_than b `2 by A7, Th29;
then A9: a2 <= b `2 by A4;
D1 is_<=_than b `1 by A7, A8, Th29;
then a1 <= b `1 by A6;
hence a <= b by A8, A9, Th11; :: thesis: verum

end;

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

end;

assume ex_sup_of [:D1,D2:],[:S1,S2:] ; :: thesis: ( ex_sup_of D1,S1 & ex_sup_of D2,S2 )
then consider x being Element of [:S1,S2:] such that
A10: [:D1,D2:] is_<=_than x and
A11: for b being Element of [:S1,S2:] st [:D1,D2:] is_<=_than b holds
x <= b by YELLOW_0:15;
the carrier of [:S1,S2:] = [: the carrier of S1, the carrier of S2:] by Def2;
then A12: x = [(x `1),(x `2)] by MCART_1:21;
then A13: D1 is_<=_than x `1 by A10, Th29;
A14: D2 is_<=_than x `2 by A10, A12, Th29;
for b being Element of S1 st D1 is_<=_than b holds
x `1 <= b

proof

let b be Element of S1; :: thesis: ( D1 is_<=_than b implies x `1 <= b )
assume D1 is_<=_than b ; :: thesis: x `1 <= b
then x <= [b,(x `2)] by A11, A14, Th30;
hence x `1 <= b by A12, Th11; :: thesis: verum

end;

hence ex_sup_of D1,S1 by A13, YELLOW_0:15; :: thesis: ex_sup_of D2,S2
for b being Element of S2 st D2 is_<=_than b holds
x `2 <= b

proof

let b be Element of S2; :: thesis: ( D2 is_<=_than b implies x `2 <= b )
assume D2 is_<=_than b ; :: thesis: x `2 <= b
then x <= [(x `1),b] by A11, A13, Th30;
hence x `2 <= b by A12, Th11; :: thesis: verum

end;

hence ex_sup_of D2,S2 by A14, YELLOW_0:15; :: thesis: verum