let X be Subset of REAL ; :: thesis: ( X is bounded_above iff - X is bounded_below )
X = - (- X) ;
hence ( X is bounded_above iff - X is bounded_below ) by Lm1, Lm2; :: thesis: verum