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