let X be set ; :: thesis: for B being SetSequence of X st B is non-ascending holds
( B is convergent & lim B = Intersection B )
let B be SetSequence of X; :: thesis: ( B is non-ascending implies ( B is convergent & lim B = Intersection B ) )
assume A0: B is non-ascending ; :: thesis: ( B is convergent & lim B = Intersection B )
then ( lim_sup B = Intersection B & lim_inf B = Intersection B ) by Th38, Th42;
hence B is convergent by KURATO_2:def 7; :: thesis: lim B = Intersection B
thus lim B = Intersection B by A0, Th38; :: thesis: verum