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

( B is convergent & lim B = Intersection B )

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

assume A1: B is V55() ; :: thesis: ( B is convergent & lim B = Intersection B )

then ( lim_sup B = Intersection B & lim_inf B = Intersection B ) by Th49, Th53;

hence B is convergent by KURATO_0:def 5; :: thesis: lim B = Intersection B

thus lim B = Intersection B by A1, Th49; :: thesis: verum

( B is convergent & lim B = Intersection B )

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

assume A1: B is V55() ; :: thesis: ( B is convergent & lim B = Intersection B )

then ( lim_sup B = Intersection B & lim_inf B = Intersection B ) by Th49, Th53;

hence B is convergent by KURATO_0:def 5; :: thesis: lim B = Intersection B

thus lim B = Intersection B by A1, Th49; :: thesis: verum