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