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_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; 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; ( ( ex_sup_of D1,S1 & ex_sup_of D2,S2 ) iff ex_sup_of [:D1,D2:],[:S1,S2:] )
hereby ( ex_sup_of [:D1,D2:],[:S1,S2:] implies ( ex_sup_of D1,S1 & ex_sup_of D2,S2 ) )
assume that A1:
ex_sup_of D1,
S1
and A2:
ex_sup_of D2,
S2
;
ex_sup_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:15;
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: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];
( [: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, Th30;
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, Th29;
then A9:
a2 <= b `2
by A4;
D1 is_<=_than b `1
by A7, A8, Th29;
then
a1 <= b `1
by A6;
hence
a <= b
by A8, A9, Th11;
verum
end; hence
ex_sup_of [:D1,D2:],
[:S1,S2:]
by YELLOW_0:15;
verum
end;
assume
ex_sup_of [:D1,D2:],[:S1,S2:]
; ( ex_sup_of D1,S1 & ex_sup_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:15;
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, Th29;
A14:
D2 is_<=_than x `2
by A10, A12, Th29;
for b being Element of S1 st D1 is_<=_than b holds
x `1 <= b
hence
ex_sup_of D1,S1
by A13, YELLOW_0:15; ex_sup_of D2,S2
for b being Element of S2 st D2 is_<=_than b holds
x `2 <= b
hence
ex_sup_of D2,S2
by A14, YELLOW_0:15; verum