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 )

hence not X is empty by Th38, Th39; :: thesis: verum

thus ( not X is empty implies inf X <= sup X ) :: thesis: ( inf X <= sup X implies not X is empty )

proof

assume
inf X <= sup X
; :: thesis: not X is empty
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;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

hence not X is empty by Th38, Th39; :: thesis: verum