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