theorem Th66: :: SETLIM_2:66

for X being set
for A1, A2 being SetSequence of X st A1 is convergent & A2 is convergent holds
lim_inf (A1 (\+\) A2) = (lim_inf A1) \+\ (lim_inf A2)