:: deftheorem Def1 defines Lim_inf KURATO_2:def 1 :
for T being non empty TopSpace
for S being SetSequence of the carrier of T
for b₃ being Subset of T holds
( b₃ = Lim_inf S iff for p being Point of T holds
( p in b₃ iff for G being a_neighborhood of p ex k being Nat st
for m being Nat st m > k holds
S . m meets G ) );