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 A1: ( ex_sup_of D1,S1 & ex_sup_of D2,S2 ) ; :: thesis: ex_sup_of [:D1,D2:],[:S1,S2:]
then consider a1 being Element of S1 such that
A2: D1 is_<=_than a1 and
A3: for b being Element of S1 st D1 is_<=_than b holds
a1 <= b by YELLOW_0:15;
consider a2 being Element of S2 such that
A4: D2 is_<=_than a2 and
A5: for b being Element of S2 st D2 is_<=_than b holds
a2 <= 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 A2, A4, 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 A6: [:D1,D2:] is_<=_than b ; :: thesis: a <= b
the carrier of [:S1,S2:] = [:the carrier of S1,the carrier of S2:] by Def2;
then A7: b = [(b `1 ),(b `2 )] by MCART_1:23;
then ( D1 is_<=_than b `1 & D2 is_<=_than b `2 ) by A6, Th29;
then ( a1 <= b `1 & a2 <= b `2 ) by A3, A5;
hence a <= b by A7, 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
A8: [:D1,D2:] is_<=_than x and
A9: 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 A10: x = [(x `1 ),(x `2 )] by MCART_1:23;
then A11: D1 is_<=_than x `1 by A8, Th29;
A12: D2 is_<=_than x `2 by A8, A10, 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 A9, A12, Th30;
hence x `1 <= b by A10, Th11; :: thesis: verum

end;

hence ex_sup_of D1,S1 by A11, 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 A9, A11, Th30;
hence x `2 <= b by A10, Th11; :: thesis: verum

end;

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