let X be Subset of REAL; :: thesis: ( X is bounded_below implies -- X is bounded_above )
given s being Real such that A1: s is LowerBound of X ; :: according to XXREAL_2:def 9 :: thesis: -- X is bounded_above
take - s ; :: according to XXREAL_2:def 10 :: thesis: - s is UpperBound of -- X
let t be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not t in -- X or t <= - s )
assume t in -- X ; :: thesis: t <= - s
then consider r3 being Complex such that
A2: t = - r3 and
A3: r3 in X ;
reconsider r3 = r3 as Real by A3;
r3 >= s by A1, A3, XXREAL_2:def 2;
hence t <= - s by A2, XREAL_1:24; :: thesis: verum