set IT = [:X,Y:];
for D being Subset of [:X,Y:] holds ex_sup_of D,[:X,Y:]
proof
let D be Subset of [:X,Y:]; :: thesis: ex_sup_of D,[:X,Y:]
( ex_sup_of proj1 D,X & ex_sup_of proj2 D,Y ) by YELLOW_0:17;
hence ex_sup_of D,[:X,Y:] by Th41; :: thesis: verum
end;
hence [:X,Y:] is complete by YELLOW_0:53; :: thesis: verum