let X, 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 Element of NAT ex k being Element of 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 Element of NAT ex k being Element of NAT st x in S . (n + k) )
let S be SetSequence of Si; :: thesis: ( x in lim_sup S iff for n being Element of NAT ex k being Element of NAT st x in S . (n + k) )
for B being SetSequence of X holds
( x in Intersection (superior_setsequence B) iff for n being Element of NAT ex k being Element of 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 Element of NAT ex k being Element of 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 Element of NAT ex k being Element of NAT st x in B . (n + k) ) by KURATO_2:8; :: thesis: verum

end;

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