let X be Subset of REAL; :: thesis: ( X is real-bounded & not X is empty implies lower_bound X <= upper_bound X )
assume ( X is real-bounded & not X is empty ) ; :: thesis: lower_bound X <= upper_bound X
then reconsider X = X as non empty real-membered real-bounded set ;
lower_bound X <= upper_bound X by XXREAL_2:40;
hence lower_bound X <= upper_bound X ; :: thesis: verum