theorem Th63: :: SETLIM_1:63

for X being set
for B being SetSequence of X st B is non-descending holds
( B is convergent & lim B = Union B )