let x be object ; :: thesis: for X being set
for Si being SigmaField of X
for S being SetSequence of Si holds
( x in lim_sup S iff for n being Nat ex k being Nat st x in S . (n + k) )
let X be set ; :: thesis: for Si being SigmaField of X
for S being SetSequence of Si holds
( x in lim_sup S iff for n being Nat ex k being Nat st x in S . (n + k) )
let Si be SigmaField of X; :: thesis: for S being SetSequence of Si holds
( x in lim_sup S iff for n being Nat ex k being Nat st x in S . (n + k) )
let S be SetSequence of Si; :: thesis: ( x in lim_sup S iff for n being Nat ex k being Nat st x in S . (n + k) )
for B being SetSequence of X holds
( x in Intersection (superior_setsequence B) iff for n being Nat ex k being Nat st x in B . (n + k) )

proof

let B be SetSequence of X; :: thesis: ( x in Intersection (superior_setsequence B) iff for n being Nat ex k being Nat st x in B . (n + k) )
lim_sup B = Intersection (superior_setsequence B) ;
hence ( x in Intersection (superior_setsequence B) iff for n being Nat ex k being Nat st x in B . (n + k) ) by KURATO_0:5; :: thesis: verum

end;

hence ( x in lim_sup S iff for n being Nat ex k being Nat st x in S . (n + k) ) ; :: thesis: verum