theorem Th36: :: RINFSUP2:36

for seq being ExtREAL_sequence st seq is non-increasing holds
( seq is convergent & lim seq = inf seq )