theorem Th63: :: SETLIM_2:63

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