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