theorem :: SETLIM_1:74

for X being set
for Si being SigmaField of X
for S1, S2, S3 being SetSequence of Si st ( for n being Nat holds S3 . n = (S1 . n) /\ (S2 . n) ) holds
lim_inf S3 = (lim_inf S1) /\ (lim_inf S2)