theorem :: SETLIM_1:69

for X being set
for Si being SigmaField of X
for S being SetSequence of Si holds lim_sup S c= Union S