theorem :: SETLIM_1:75

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