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