theorem Th66: :: SETLIM_1:66

for x being object
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) )