theorem Th11: :: PROB_4:11

for seq being sequence of REAL
for Eseq being sequence of ExtREAL st seq = Eseq & seq is V110() holds
lower_bound seq = inf (rng Eseq)