let X be ext-real-membered set ; :: thesis: ( not X is empty iff inf X <= sup X )
thus ( not X is empty implies inf X <= sup X ) :: thesis: ( inf X <= sup X implies not X is empty )
proof
assume not X is empty ; :: thesis: inf X <= sup X
then consider x being ExtReal such that
A1: x in X by MEMBERED:8;
A2: x <= sup X by A1, Th4;
inf X <= x by A1, Th3;
hence inf X <= sup X by A2, XXREAL_0:2; :: thesis: verum
end;
assume inf X <= sup X ; :: thesis: not X is empty
hence not X is empty by Th38, Th39; :: thesis: verum