theorem :: SETLIM_1:76

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_sup S3 c= (lim_sup S1) /\ (lim_sup S2)