let X be set ; :: thesis: for Si being SigmaField of X

for ASeq being SetSequence of Si holds Union ASeq in Si

let Si be SigmaField of X; :: thesis: for ASeq being SetSequence of Si holds Union ASeq in Si

let ASeq be SetSequence of Si; :: thesis: Union ASeq in Si

A1: for A1 being SetSequence of X st rng A1 c= Si holds

for n being Nat holds (Complement A1) . n in Si

Union (Complement (Complement A1)) in Si

Union A1 in Si

hence Union ASeq in Si by A4; :: thesis: verum

for ASeq being SetSequence of Si holds Union ASeq in Si

let Si be SigmaField of X; :: thesis: for ASeq being SetSequence of Si holds Union ASeq in Si

let ASeq be SetSequence of Si; :: thesis: Union ASeq in Si

A1: for A1 being SetSequence of X st rng A1 c= Si holds

for n being Nat holds (Complement A1) . n in Si

proof

A3:
for A1 being SetSequence of X st rng A1 c= Si holds
let A1 be SetSequence of X; :: thesis: ( rng A1 c= Si implies for n being Nat holds (Complement A1) . n in Si )

assume A2: rng A1 c= Si ; :: thesis: for n being Nat holds (Complement A1) . n in Si

let n be Nat; :: thesis: (Complement A1) . n in Si

A1 . n in rng A1 by NAT_1:51;

then ( n in NAT & (A1 . n) ` in Si ) by A2, Def1, ORDINAL1:def 12;

hence (Complement A1) . n in Si by Def2; :: thesis: verum

end;assume A2: rng A1 c= Si ; :: thesis: for n being Nat holds (Complement A1) . n in Si

let n be Nat; :: thesis: (Complement A1) . n in Si

A1 . n in rng A1 by NAT_1:51;

then ( n in NAT & (A1 . n) ` in Si ) by A2, Def1, ORDINAL1:def 12;

hence (Complement A1) . n in Si by Def2; :: thesis: verum

Union (Complement (Complement A1)) in Si

proof

A4:
for A1 being SetSequence of X st rng A1 c= Si holds
let A1 be SetSequence of X; :: thesis: ( rng A1 c= Si implies Union (Complement (Complement A1)) in Si )

assume rng A1 c= Si ; :: thesis: Union (Complement (Complement A1)) in Si

then for n being Nat holds (Complement A1) . n in Si by A1;

then rng (Complement A1) c= Si by NAT_1:52;

then Intersection (Complement A1) in Si by Def6;

then ((Union (Complement (Complement A1))) `) ` in Si by Def1;

hence Union (Complement (Complement A1)) in Si ; :: thesis: verum

end;assume rng A1 c= Si ; :: thesis: Union (Complement (Complement A1)) in Si

then for n being Nat holds (Complement A1) . n in Si by A1;

then rng (Complement A1) c= Si by NAT_1:52;

then Intersection (Complement A1) in Si by Def6;

then ((Union (Complement (Complement A1))) `) ` in Si by Def1;

hence Union (Complement (Complement A1)) in Si ; :: thesis: verum

Union A1 in Si

proof

rng ASeq c= Si
by RELAT_1:def 19;
let A1 be SetSequence of X; :: thesis: ( rng A1 c= Si implies Union A1 in Si )

assume rng A1 c= Si ; :: thesis: Union A1 in Si

then Union (Complement (Complement A1)) in Si by A3;

hence Union A1 in Si ; :: thesis: verum

end;assume rng A1 c= Si ; :: thesis: Union A1 in Si

then Union (Complement (Complement A1)) in Si by A3;

hence Union A1 in Si ; :: thesis: verum

hence Union ASeq in Si by A4; :: thesis: verum