let X be Subset of REAL ; :: thesis: ( X is bounded_below implies -- X is bounded_above )
given s being real number 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 ext-real number ; :: according to XXREAL_2:def 1 :: thesis: ( not t in -- X or t <= - s )
assume t in -- X ; :: thesis: t <= - s
then t in { (- r2) where r2 is Element of COMPLEX : r2 in X } by MEMBER_1:def 2;
then consider r2 being Element of COMPLEX such that
A2: t = - r2 and
A3: r2 in X ;
reconsider r3 = r2 as Real by A3;
r3 >= s by A1, A3, XXREAL_2:def 2;
hence t <= - s by A2, XREAL_1:26; :: thesis: verum