let seq be Real_Sequence; :: thesis: ( seq is bounded implies upper_bound (inferior_realsequence seq) <= lower_bound (superior_realsequence seq) )
set seq1 = inferior_realsequence seq;
set r = lower_bound (superior_realsequence seq);
assume seq is bounded ; :: thesis: upper_bound (inferior_realsequence seq) <= lower_bound (superior_realsequence seq)
then for n being Nat holds (inferior_realsequence seq) . n <= lower_bound (superior_realsequence seq) by Th53;
hence upper_bound (inferior_realsequence seq) <= lower_bound (superior_realsequence seq) by Th9; :: thesis: verum