theorem Th5: :: KURATO_0:5

for X being set
for F being SetSequence of X
for x being object holds
( x in lim_sup F iff for n being Nat ex k being Nat st x in F . (n + k) )