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

let X be non empty directed Subset of T; :: according to WAYBEL_0:def 39 :: thesis: ex b_{1} being Element of the carrier of T st

( X is_<=_than b_{1} & ( for b_{2} being Element of the carrier of T holds

( not X is_<=_than b_{2} or b_{1} <= b_{2} ) ) )

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 ; :: thesis: ( X is_<=_than x `2 & ( for b_{1} being Element of the carrier of T holds

( not X is_<=_than b_{1} or x `2 <= b_{1} ) ) )

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; :: thesis: for b_{1} being Element of the carrier of T holds

( not X is_<=_than b_{1} or x `2 <= b_{1} )

let y be Element of T; :: thesis: ( not X is_<=_than y or x `2 <= y )

assume y is_>=_than X ; :: thesis: 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; :: thesis: verum

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

set D = the non empty directed Subset of S;
set D = the non empty directed Subset of T;

let X be non empty directed Subset of S; :: according to WAYBEL_0:def 39 :: thesis: ex b_{1} being Element of the carrier of S st

( X is_<=_than b_{1} & ( for b_{2} being Element of the carrier of S holds

( not X is_<=_than b_{2} or b_{1} <= b_{2} ) ) )

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 ; :: thesis: ( X is_<=_than x `1 & ( for b_{1} being Element of the carrier of S holds

( not X is_<=_than b_{1} or x `1 <= b_{1} ) ) )

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; :: thesis: for b_{1} being Element of the carrier of S holds

( not X is_<=_than b_{1} or x `1 <= b_{1} )

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; :: thesis: ( not X is_<=_than y or x `1 <= y )

assume y is_>=_than X ; :: thesis: 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; :: thesis: verum

end;let X be non empty directed Subset of S; :: according to WAYBEL_0:def 39 :: thesis: ex b

( X is_<=_than b

( not X is_<=_than b

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 ; :: thesis: ( X is_<=_than x `1 & ( for b

( not X is_<=_than b

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; :: thesis: for b

( not X is_<=_than b

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; :: thesis: ( not X is_<=_than y or x `1 <= y )

assume y is_>=_than X ; :: thesis: 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; :: thesis: verum

let X be non empty directed Subset of T; :: according to WAYBEL_0:def 39 :: thesis: ex b

( X is_<=_than b

( not X is_<=_than b

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 ; :: thesis: ( X is_<=_than x `2 & ( for b

( not X is_<=_than b

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; :: thesis: for b

( not X is_<=_than b

let y be Element of T; :: thesis: ( not X is_<=_than y or x `2 <= y )

assume y is_>=_than X ; :: thesis: 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; :: thesis: verum