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;
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;
end;
end;
hence Y is complete by YELLOW_0:53; :: thesis: verum