theorem Th60: :: SETLIM_2:60

for X being set
for A1, A2 being SetSequence of X holds lim_inf (A1 (/\) A2) = (lim_inf A1) /\ (lim_inf A2)