for X being Subset of REAL st X is real-bounded & not X is empty holds
( ex r, p being Real st
( r in X & p in X & p <> r ) iff lower_bound X < upper_bound X )