sup X in REAL by Th16;
hence sup X is real ; :: thesis: