let X be set ; :: thesis: for Si being SigmaField of X
for S being SetSequence of st S is non-ascending holds
lim_sup S = Intersection S
let Si be SigmaField of X; :: thesis: for S being SetSequence of st S is non-ascending holds
lim_sup S = Intersection S
let S be SetSequence of ; :: thesis: ( S is non-ascending implies lim_sup S = Intersection S )
A00: for B being SetSequence of X st B is non-ascending holds
Intersection (superior_setsequence B) = Intersection B

proof

let B be SetSequence of X; :: thesis: ( B is non-ascending implies Intersection (superior_setsequence B) = Intersection B )
lim_sup B = Intersection (superior_setsequence B) ;
hence ( B is non-ascending implies Intersection (superior_setsequence B) = Intersection B ) by Th51; :: thesis: verum

end;

thus ( S is non-ascending implies lim_sup S = Intersection S ) by A00; :: thesis: verum