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