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 Lm2, Lm3; :: thesis: verum