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

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

( S is convergent & lim S = Union S )

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

( S is convergent & lim S = Union S )

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

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

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

( S is convergent & lim S = Union S )

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

( S is convergent & lim S = Union S )

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

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