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 consider r3 being Real such that
A2: ( t = - r3 & r3 in X ) ;
r3 >= s by A1, A2, XXREAL_2:def 2;
hence t <= - s by A2, XREAL_1:26; :: thesis: verum