theorem Th4: :: KURATO_0:4

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