let X be set ; :: thesis: 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)

let Si be SigmaField of X; :: thesis: 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)

let S1, S2, S3 be SetSequence of Si; :: thesis: ( ( for n being Nat holds S3 . n = (S1 . n) \/ (S2 . n) ) implies lim_sup S3 = (lim_sup S1) \/ (lim_sup S2) )

A1: for B, A2, A3 being SetSequence of X st ( for n being Nat holds A3 . n = (B . n) \/ (A2 . n) ) holds

(Intersection (superior_setsequence B)) \/ (Intersection (superior_setsequence A2)) = Intersection (superior_setsequence A3)

hence lim_sup S3 = (lim_sup S1) \/ (lim_sup S2) by A1; :: thesis: verum

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)

let Si be SigmaField of X; :: thesis: 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)

let S1, S2, S3 be SetSequence of Si; :: thesis: ( ( for n being Nat holds S3 . n = (S1 . n) \/ (S2 . n) ) implies lim_sup S3 = (lim_sup S1) \/ (lim_sup S2) )

A1: for B, A2, A3 being SetSequence of X st ( for n being Nat holds A3 . n = (B . n) \/ (A2 . n) ) holds

(Intersection (superior_setsequence B)) \/ (Intersection (superior_setsequence A2)) = Intersection (superior_setsequence A3)

proof

assume
for n being Nat holds S3 . n = (S1 . n) \/ (S2 . n)
; :: thesis: lim_sup S3 = (lim_sup S1) \/ (lim_sup S2)
let B, A2, A3 be SetSequence of X; :: thesis: ( ( for n being Nat holds A3 . n = (B . n) \/ (A2 . n) ) implies (Intersection (superior_setsequence B)) \/ (Intersection (superior_setsequence A2)) = Intersection (superior_setsequence A3) )

A2: ( lim_sup B = Intersection (superior_setsequence B) & lim_sup A2 = Intersection (superior_setsequence A2) ) ;

A3: lim_sup A3 = Intersection (superior_setsequence A3) ;

assume for n being Nat holds A3 . n = (B . n) \/ (A2 . n) ; :: thesis: (Intersection (superior_setsequence B)) \/ (Intersection (superior_setsequence A2)) = Intersection (superior_setsequence A3)

hence (Intersection (superior_setsequence B)) \/ (Intersection (superior_setsequence A2)) = Intersection (superior_setsequence A3) by A2, A3, KURATO_0:11; :: thesis: verum

end;A2: ( lim_sup B = Intersection (superior_setsequence B) & lim_sup A2 = Intersection (superior_setsequence A2) ) ;

A3: lim_sup A3 = Intersection (superior_setsequence A3) ;

assume for n being Nat holds A3 . n = (B . n) \/ (A2 . n) ; :: thesis: (Intersection (superior_setsequence B)) \/ (Intersection (superior_setsequence A2)) = Intersection (superior_setsequence A3)

hence (Intersection (superior_setsequence B)) \/ (Intersection (superior_setsequence A2)) = Intersection (superior_setsequence A3) by A2, A3, KURATO_0:11; :: thesis: verum

hence lim_sup S3 = (lim_sup S1) \/ (lim_sup S2) by A1; :: thesis: verum