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

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₁ being Element of the carrier of S st
( X is_<=_than b₁ & ( for b₂ being Element of the carrier of S holds
( not X is_<=_than b₂ or b₁ <= 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₁ being Element of the carrier of S holds
( not X is_<=_than b₁ or x `1 <= b<sub>1</sub> ) ) )
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₁ being Element of the carrier of S holds
( not X is_<=_than b₁ or x `1 <= b<sub>1</sub> )
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;

set D = the non empty directed Subset of S;
let X be non empty directed Subset of T; :: according to WAYBEL_0:def 39 :: thesis: ex b₁ being Element of the carrier of T st
( X is_<=_than b₁ & ( for b₂ being Element of the carrier of T holds
( not X is_<=_than b₂ or b₁ <= 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₁ being Element of the carrier of T holds
( not X is_<=_than b₁ or x `2 <= b<sub>1</sub> ) ) )
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₁ being Element of the carrier of T holds
( not X is_<=_than b₁ or x `2 <= b<sub>1</sub> )
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