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_inf_of D1,S1 & ex_inf_of D2,S2 ) iff ex_inf_of [:D1,D2:],[:S1,S2:] )
let D1 be non empty Subset of S1; :: thesis: for D2 being non empty Subset of S2 holds
( ( ex_inf_of D1,S1 & ex_inf_of D2,S2 ) iff ex_inf_of [:D1,D2:],[:S1,S2:] )
let D2 be non empty Subset of S2; :: thesis: ( ( ex_inf_of D1,S1 & ex_inf_of D2,S2 ) iff ex_inf_of [:D1,D2:],[:S1,S2:] )

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

assume A1: ( ex_inf_of D1,S1 & ex_inf_of D2,S2 ) ; :: thesis: ex_inf_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:16;
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:16;
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, Th33; :: 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, Th32;
then ( a1 >= b `1 & a2 >= b `2 ) by A3, A5;
hence a >= b by A7, Th11; :: thesis: verum

end;

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

end;

assume ex_inf_of [:D1,D2:],[:S1,S2:] ; :: thesis: ( ex_inf_of D1,S1 & ex_inf_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:16;
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, Th32;
A12: D2 is_>=_than x `2 by A8, A10, Th32;
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, Th33;
hence x `1 >= b by A10, Th11; :: thesis: verum

end;

hence ex_inf_of D1,S1 by A11, YELLOW_0:16; :: thesis: ex_inf_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, Th33;
hence x `2 >= b by A10, Th11; :: thesis: verum

end;

hence ex_inf_of D2,S2 by A12, YELLOW_0:16; :: thesis: verum