theorem Th62: :: SETLIM_2:62

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