let S, T be non empty reflexive antisymmetric RelStr ; ( [:S,T:] is up-complete implies ( S is up-complete & T is up-complete ) )
assume A1:
[:S,T:] is up-complete
; ( S is up-complete & T is up-complete )
thus
S is up-complete
T is up-complete proof
set D = the non
empty directed Subset of
T;
let X be non
empty directed Subset of
S;
WAYBEL_0:def 39 ex b1 being Element of the carrier of S st
( X is_<=_than b1 & ( for b2 being Element of the carrier of S holds
( not X is_<=_than b2 or b1 <= b2 ) ) )
consider x being
Element of
[:S,T:] such that A2:
x is_>=_than [:X, the non empty directed Subset of T:]
and A3:
for
y being
Element of
[:S,T:] st
y is_>=_than [:X, the non empty directed Subset of T:] holds
x <= y
by A1;
take
x `1
;
( X is_<=_than x `1 & ( for b1 being Element of the carrier of S holds
( not X is_<=_than b1 or x `1 <= b1 ) ) )
the
carrier of
[:S,T:] = [: the carrier of S, the carrier of T:]
by YELLOW_3:def 2;
then A4:
x = [(x `1),(x `2)]
by MCART_1:21;
hence
x `1 is_>=_than X
by A2, YELLOW_3:29;
for b1 being Element of the carrier of S holds
( not X is_<=_than b1 or x `1 <= b1 )
ex_sup_of [:X, the non empty directed Subset of T:],
[:S,T:]
by A1, WAYBEL_0:75;
then
ex_sup_of the non
empty directed Subset of
T,
T
by YELLOW_3:39;
then A5:
sup the non
empty directed Subset of
T is_>=_than the non
empty directed Subset of
T
by YELLOW_0:def 9;
let y be
Element of
S;
( not X is_<=_than y or x `1 <= y )
assume
y is_>=_than X
;
x `1 <= y
then
x <= [y,(sup the non empty directed Subset of T)]
by A3, A5, YELLOW_3:30;
hence
x `1 <= y
by A4, YELLOW_3:11;
verum
end;
set D = the non empty directed Subset of S;
let X be non empty directed Subset of T; WAYBEL_0:def 39 ex b1 being Element of the carrier of T st
( X is_<=_than b1 & ( for b2 being Element of the carrier of T holds
( not X is_<=_than b2 or b1 <= b2 ) ) )
consider x being Element of [:S,T:] such that
A6:
x is_>=_than [: the non empty directed Subset of S,X:]
and
A7:
for y being Element of [:S,T:] st y is_>=_than [: the non empty directed Subset of S,X:] holds
x <= y
by A1;
ex_sup_of [: the non empty directed Subset of S,X:],[:S,T:]
by A1, WAYBEL_0:75;
then
ex_sup_of the non empty directed Subset of S,S
by YELLOW_3:39;
then A8:
sup the non empty directed Subset of S is_>=_than the non empty directed Subset of S
by YELLOW_0:def 9;
take
x `2
; ( X is_<=_than x `2 & ( for b1 being Element of the carrier of T holds
( not X is_<=_than b1 or x `2 <= b1 ) ) )
the carrier of [:S,T:] = [: the carrier of S, the carrier of T:]
by YELLOW_3:def 2;
then A9:
x = [(x `1),(x `2)]
by MCART_1:21;
hence
x `2 is_>=_than X
by A6, YELLOW_3:29; for b1 being Element of the carrier of T holds
( not X is_<=_than b1 or x `2 <= b1 )
let y be Element of T; ( not X is_<=_than y or x `2 <= y )
assume
y is_>=_than X
; x `2 <= y
then
x <= [(sup the non empty directed Subset of S),y]
by A7, A8, YELLOW_3:30;
hence
x `2 <= y
by A9, YELLOW_3:11; verum