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) )

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

hence
( x in lim_sup S iff for n being Nat ex k being Nat st x in S . (n + k) )
; :: thesis: verum
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;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