let X be set ; :: thesis: for B being SetSequence of X st B is monotone holds
B is convergent
let B be SetSequence of X; :: thesis: ( B is monotone implies B is convergent )
assume A1: B is monotone ; :: thesis: B is convergent

per cases ( not B is V49() or not B is V50() ) by A1, Def1;

suppose B is V49() ; :: thesis: B is convergent

hence B is convergent by Th64; :: thesis: verum

end;

suppose B is V50() ; :: thesis: B is convergent

hence B is convergent by Th63; :: thesis: verum

end;

end;