theorem Th78: :: SETLIM_1:78

for X being set
for Si being SigmaField of X
for S being SetSequence of Si st S is non-descending holds
lim_sup S = Union S by Th43;