let seq be Real_Sequence; :: thesis: ( seq is bounded implies sup (inferior_realsequence seq) <= inf (superior_realsequence seq) )
set seq1 = inferior_realsequence seq;
set r = inf (superior_realsequence seq);
assume seq is bounded ; :: thesis: sup (inferior_realsequence seq) <= inf (superior_realsequence seq)
then for n being Element of NAT holds (inferior_realsequence seq) . n <= inf (superior_realsequence seq) by Th55;
hence sup (inferior_realsequence seq) <= inf (superior_realsequence seq) by Th9; :: thesis: verum