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 Th77; :: thesis: verum