let X be Subset of REAL; :: thesis: ( X is bounded_above implies -- X is bounded_below )
given s being Real such that A1: s is UpperBound of X ; :: according to XXREAL_2:def 10 :: thesis: -- X is bounded_below
take - s ; :: according to XXREAL_2:def 9 :: thesis: - s is LowerBound of -- X
let t be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not t in -- X or - s <= t )
assume t in -- X ; :: thesis: - s <= t
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 1;
hence - s <= t by A2, XREAL_1:24; :: thesis: verum