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

proof

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;

A3: for A1 being SetSequence of X st rng A1 c= Si holds
Union (Complement (Complement A1)) in Si

proof

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;

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

proof

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;

rng ASeq c= Si by RELAT_1:def 19;
hence Union ASeq in Si by A4; :: thesis: verum