let S1, S2 be non empty antisymmetric RelStr ; for D being Subset of [:S1,S2:] holds
( ( ex_inf_of proj1 D,S1 & ex_inf_of proj2 D,S2 ) iff ex_inf_of D,[:S1,S2:] )
let D be Subset of [:S1,S2:]; ( ( ex_inf_of proj1 D,S1 & ex_inf_of proj2 D,S2 ) iff ex_inf_of D,[:S1,S2:] )
A1:
the carrier of [:S1,S2:] = [: the carrier of S1, the carrier of S2:]
by Def2;
then A2:
D c= [:(proj1 D),(proj2 D):]
by Th1;
hereby ( ex_inf_of D,[:S1,S2:] implies ( ex_inf_of proj1 D,S1 & ex_inf_of proj2 D,S2 ) )
assume that A3:
ex_inf_of proj1 D,
S1
and A4:
ex_inf_of proj2 D,
S2
;
ex_inf_of D,[:S1,S2:]
ex
a being
Element of
[:S1,S2:] st
(
D is_>=_than a & ( for
b being
Element of
[:S1,S2:] st
D is_>=_than b holds
a >= b ) )
proof
consider x2 being
Element of
S2 such that A5:
proj2 D is_>=_than x2
and A6:
for
b being
Element of
S2 st
proj2 D is_>=_than b holds
x2 >= b
by A4, YELLOW_0:16;
consider x1 being
Element of
S1 such that A7:
proj1 D is_>=_than x1
and A8:
for
b being
Element of
S1 st
proj1 D is_>=_than b holds
x1 >= b
by A3, YELLOW_0:16;
take a =
[x1,x2];
( D is_>=_than a & ( for b being Element of [:S1,S2:] st D is_>=_than b holds
a >= b ) )
thus
D is_>=_than a
for b being Element of [:S1,S2:] st D is_>=_than b holds
a >= b
let b be
Element of
[:S1,S2:];
( D is_>=_than b implies a >= b )
assume A12:
D is_>=_than b
;
a >= b
A13:
b = [(b `1),(b `2)]
by A1, MCART_1:21;
then
proj2 D is_>=_than b `2
by A12, Th34;
then A14:
x2 >= b `2
by A6;
proj1 D is_>=_than b `1
by A12, A13, Th34;
then
x1 >= b `1
by A8;
hence
a >= b
by A13, A14, Th11;
verum
end; hence
ex_inf_of D,
[:S1,S2:]
by YELLOW_0:16;
verum
end;
assume
ex_inf_of D,[:S1,S2:]
; ( ex_inf_of proj1 D,S1 & ex_inf_of proj2 D,S2 )
then consider x being Element of [:S1,S2:] such that
A15:
D is_>=_than x
and
A16:
for b being Element of [:S1,S2:] st D is_>=_than b holds
x >= b
by YELLOW_0:16;
A17:
x = [(x `1),(x `2)]
by A1, MCART_1:21;
then A18:
proj1 D is_>=_than x `1
by A15, Th34;
A19:
proj2 D is_>=_than x `2
by A15, A17, Th34;
for b being Element of S1 st proj1 D is_>=_than b holds
x `1 >= b
hence
ex_inf_of proj1 D,S1
by A18, YELLOW_0:16; ex_inf_of proj2 D,S2
for b being Element of S2 st proj2 D is_>=_than b holds
x `2 >= b
hence
ex_inf_of proj2 D,S2
by A19, YELLOW_0:16; verum