let X be Subset of REAL ; :: thesis: ( X is bounded_above implies - X is bounded_below )
given s being real number 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 ext-real number ; :: 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 Real such that
A2: ( t = - r3 & r3 in X ) ;
r3 <= s by A1, A2, XXREAL_2:def 1;
hence - s <= t by A2, XREAL_1:26; :: thesis: verum