let X be set ; :: thesis: for Si being SigmaField of X

for S being SetSequence of Si st S is monotone holds

S is convergent

let Si be SigmaField of X; :: thesis: for S being SetSequence of Si st S is monotone holds

S is convergent

let S be SetSequence of Si; :: thesis: ( S is monotone implies S is convergent )

assume A1: S is monotone ; :: thesis: S is convergent

for S being SetSequence of Si st S is monotone holds

S is convergent

let Si be SigmaField of X; :: thesis: for S being SetSequence of Si st S is monotone holds

S is convergent

let S be SetSequence of Si; :: thesis: ( S is monotone implies S is convergent )

assume A1: S is monotone ; :: thesis: S is convergent