inf X in REAL by Th15;
hence inf X is real ; :: thesis: