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 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 ; :: 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:21;
hence x `1 is_>=_than X by ; :: thesis: 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 ;
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 ;
hence x `1 <= y by ; :: 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 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 ;
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 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 ; :: 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 y is_>=_than X ; :: thesis: x `2 <= y
then x <= [(sup the non empty directed Subset of S),y] by ;
hence x `2 <= y by ; :: thesis: verum