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