theorem Th61: :: SETLIM_2:61

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