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 A1: B is non-ascending ; :: 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