let X be set ; :: thesis: for B being SetSequence of X st B is V56() holds

( B is convergent & lim B = Union B )

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

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

( B is convergent & lim B = Union B )

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

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