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