theorem :: KURATO_0:10

for X being set
for A, B, C being SetSequence of X st ( for n being Nat holds C . n = (A . n) /\ (B . n) ) holds
lim_inf C = (lim_inf A) /\ (lim_inf B)