theorem Th38: :: MEASURE6:38

for seq being Real_Sequence st seq is convergent & seq is non-zero & lim seq = 0 holds
not seq " is bounded