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

per cases ( not S is non-ascending or not S is non-descending ) by A1;

suppose S is non-ascending ; :: thesis: S is convergent

hence S is convergent by Th83; :: thesis: verum

end;

suppose S is non-descending ; :: thesis: S is convergent

hence S is convergent by Th80; :: thesis: verum

end;

end;