theorem :: SEQ_4:11

for X being Subset of REAL st X is real-bounded & not X is empty holds
lower_bound X <= upper_bound X