let seq be Real_Sequence; :: thesis: ( seq is bounded_below iff - seq is bounded_above )
- (- seq) = seq ;
hence ( seq is bounded_below iff - seq is bounded_above ) ; :: thesis: verum