theorem :: KURATO_0:12

for X being set
for A, B, C being SetSequence of X st ( for n being Nat holds C . n = (A . n) \/ (B . n) ) holds
(lim_inf A) \/ (lim_inf B) c= lim_inf C