theorem :: SETLIM_1:84

for X being set
for Si being SigmaField of X
for S being SetSequence of Si st S is monotone holds
S is convergent