let S1, S2 be non empty antisymmetric RelStr ; 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; 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; ( ( ex_inf_of D1,S1 & ex_inf_of D2,S2 ) iff ex_inf_of [:D1,D2:],[:S1,S2:] )
hereby ( 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
;
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];
( [: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;
for b being Element of [:S1,S2:] st [:D1,D2:] is_>=_than b holds
a >= b
let b be
Element of
[:S1,S2:];
( [:D1,D2:] is_>=_than b implies a >= b )
assume A7:
[:D1,D2:] is_>=_than b
;
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;
verum
end; hence
ex_inf_of [:D1,D2:],
[:S1,S2:]
by YELLOW_0:16;
verum
end;
assume
ex_inf_of [:D1,D2:],[:S1,S2:]
; ( 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
hence
ex_inf_of D1,S1
by A13, YELLOW_0:16; ex_inf_of D2,S2
for b being Element of S2 st D2 is_>=_than b holds
x `2 >= b
hence
ex_inf_of D2,S2
by A14, YELLOW_0:16; verum