let X, Y be non empty antisymmetric lower-bounded RelStr ; :: thesis: ( [:X,Y:] is complete implies ( X is complete & Y is complete ) )
assume A1: [:X,Y:] is complete ; :: thesis: ( X is complete & Y is complete )
for A being Subset of X holds ex_sup_of A,X

proof

let A be Subset of X; :: thesis: ex_sup_of A,X

per cases ( not A is empty or A is empty ) ;

suppose A2: not A is empty ; :: thesis: ex_sup_of A,X

set B = the non empty Subset of Y;
ex_sup_of [:A, the non empty Subset of Y:],[:X,Y:] by A1, YELLOW_0:17;
hence ex_sup_of A,X by A2, Th39; :: thesis: verum

end;

suppose A is empty ; :: thesis: ex_sup_of A,X

hence ex_sup_of A,X by YELLOW_0:42; :: thesis: verum

end;

end;

end;

hence X is complete by YELLOW_0:53; :: thesis: Y is complete
for B being Subset of Y holds ex_sup_of B,Y

proof

let B be Subset of Y; :: thesis: ex_sup_of B,Y

per cases ( not B is empty or B is empty ) ;

suppose A3: not B is empty ; :: thesis: ex_sup_of B,Y

set A = the non empty Subset of X;
ex_sup_of [: the non empty Subset of X,B:],[:X,Y:] by A1, YELLOW_0:17;
hence ex_sup_of B,Y by A3, Th39; :: thesis: verum

end;

suppose B is empty ; :: thesis: ex_sup_of B,Y

hence ex_sup_of B,Y by YELLOW_0:42; :: thesis: verum

end;

end;

end;

hence Y is complete by YELLOW_0:53; :: thesis: verum