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

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