theorem :: RINFSUP1:87

for seq being Real_Sequence st seq is bounded holds
lim_inf seq <= lim_sup seq by Th55;