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 V55() or not S is V56() ) by A1;
suppose S is V55() ; :: thesis: S is convergent
hence S is convergent by Th83; :: thesis: verum
end;
suppose S is V56() ; :: thesis: S is convergent
hence S is convergent by Th80; :: thesis: verum
end;
end;