:: deftheorem Def1 defines lim_inf KURATO_0:def 1 :
for X being set
for F being SetSequence of X
for b₃ being Subset of X holds
( b₃ = lim_inf F iff ex f being SetSequence of X st
( b₃ = Union f & ( for n being Nat holds f . n = meet (F ^\ n) ) ) );