let seq be Real_Sequence; :: thesis: ( seq is bounded_above iff - seq is bounded_below )
set seq1 = - seq;
thus ( seq is bounded_above implies - seq is bounded_below ) ; :: thesis: ( - seq is bounded_below implies seq is bounded_above )
assume - seq is bounded_below ; :: thesis: seq is bounded_above
then consider t being Real such that
A1: for n being Nat holds (- seq) . n > t by SEQ_2:def 4;
for n being Nat holds seq . n < - t

proof

let n be Nat; :: thesis: seq . n < - t
(- seq) . n = - (seq . n) by SEQ_1:10;
then A2: - ((- seq) . n) = seq . n ;
(- seq) . n > t by A1;
hence seq . n < - t by A2, XREAL_1:24; :: thesis: verum

end;

hence seq is bounded_above by SEQ_2:def 3; :: thesis: verum