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