begin
Lm1:
for seq being ExtREAL_sequence holds superior_realsequence seq is non-increasing
Lm2:
for seq being ExtREAL_sequence holds inferior_realsequence seq is non-decreasing
Lm3:
for seq being ExtREAL_sequence st seq is bounded & seq is non-increasing holds
( seq is convergent_to_finite_number & seq is convergent & lim seq = inf seq )
Lm4:
for seq being ExtREAL_sequence st seq is bounded & seq is non-decreasing holds
( seq is convergent_to_finite_number & seq is convergent & lim seq = sup seq )
Lm5:
for seq being ExtREAL_sequence st lim_inf seq = lim_sup seq & lim_inf seq = +infty holds
( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq )
Lm6:
for seq being ExtREAL_sequence st lim_inf seq = lim_sup seq & lim_inf seq = -infty holds
( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq )
Lm7:
for seq being ExtREAL_sequence st lim_inf seq = lim_sup seq & lim_inf seq in REAL holds
( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq )