let X be set ; :: thesis: for B being SetSequence of X st B is non-descending holds
( B is convergent & lim B = Union B )
let B be SetSequence of X; :: thesis: ( B is non-descending implies ( B is convergent & lim B = Union B ) )
assume A1: B is non-descending ; :: thesis: ( B is convergent & lim B = Union B )
then ( lim_sup B = Union B & lim_inf B = Union B ) by Th43, Th46;
hence B is convergent by KURATO_0:def 5; :: thesis: lim B = Union B
thus lim B = Union B by A1, Th43; :: thesis: verum