let seq be Real_Sequence; :: thesis: ( seq is bounded_below implies inferior_realsequence seq = - (superior_realsequence (- seq)) )
assume seq is bounded_below ; :: thesis: inferior_realsequence seq = - (superior_realsequence (- seq))
then for n being Nat holds (inferior_realsequence seq) . n = - ((superior_realsequence (- seq)) . n) by Th59;
hence inferior_realsequence seq = - (superior_realsequence (- seq)) by SEQ_1:10; :: thesis: verum