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 ext-real number such that
W: x in X by MEMBERED:8;
( inf X <= x & x <= sup X ) by W, Th3, Th3B;
hence inf X <= sup X by XXREAL_0:2; :: thesis: verum

end;

assume inf X <= sup X ; :: thesis: not X is empty
hence not X is empty by TW3, TW4; :: thesis: verum