let X be set ; :: thesis: for Si being SigmaField of X

for S being SetSequence of Si st S is V55() holds

( S is convergent & lim S = Intersection S )

let Si be SigmaField of X; :: thesis: for S being SetSequence of Si st S is V55() holds

( S is convergent & lim S = Intersection S )

let S be SetSequence of Si; :: thesis: ( S is V55() implies ( S is convergent & lim S = Intersection S ) )

assume A1: S is V55() ; :: 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

for S being SetSequence of Si st S is V55() holds

( S is convergent & lim S = Intersection S )

let Si be SigmaField of X; :: thesis: for S being SetSequence of Si st S is V55() holds

( S is convergent & lim S = Intersection S )

let S be SetSequence of Si; :: thesis: ( S is V55() implies ( S is convergent & lim S = Intersection S ) )

assume A1: S is V55() ; :: 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