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 that
A1: ex_inf_of D1,S1 and
A2: ex_inf_of D2,S2 ; :: thesis: ex_inf_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:16;
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: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 A5, A3, 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 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, Th32;
then A9: a2 >= b `2 by A4;
D1 is_>=_than b `1 by A7, A8, Th32;
then a1 >= b `1 by A6;
hence a >= b by A8, A9, 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
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:16;
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, Th32;
A14: D2 is_>=_than x `2 by A10, A12, 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 A11, A14, Th33;
hence x `1 >= b by A12, Th11; :: thesis: verum
end;
hence ex_inf_of D1,S1 by A13, 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 A11, A13, Th33;
hence x `2 >= b by A12, Th11; :: thesis: verum
end;
hence ex_inf_of D2,S2 by A14, YELLOW_0:16; :: thesis: verum