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