A1: for f being SetSequence of Omega st rng f c= DynSys X,G & f is disjoint_valued holds
Union f in DynSys X,G

proof

reconsider X1 = X as Subset of Omega ;
let f be SetSequence of Omega; :: thesis: ( rng f c= DynSys X,G & f is disjoint_valued implies Union f in DynSys X,G )
assume that
A2: rng f c= DynSys X,G and
A3: f is disjoint_valued ; :: thesis: Union f in DynSys X,G

now

let x be set ; :: thesis: ( x in rng (seqIntersection X1,f) implies x in G )
assume x in rng (seqIntersection X1,f) ; :: thesis: x in G
then consider n being Element of NAT such that
A4: x = (seqIntersection X1,f) . n by Th1;
A5: f . n in rng f by Th1;
x = X /\ (f . n) by A4, Def2;
hence x in G by A2, A5, Def9; :: thesis: verum

end;

then A6: rng (seqIntersection X1,f) c= G by TARSKI:def 3;
seqIntersection X,f is disjoint_valued by A3, Th12;
then Union (seqIntersection X1,f) in G by A6, Def7;
then X /\ (Union f) in G by Th13;
hence Union f in DynSys X,G by Def9; :: thesis: verum

end;

A7: for A being Subset of Omega st A in DynSys X,G holds
A ` in DynSys X,G

proof

let A be Subset of Omega; :: thesis: ( A in DynSys X,G implies A ` in DynSys X,G )
X misses X ` by XBOOLE_1:79;
then A8: X /\ (X ` ) = {} by XBOOLE_0:def 7;
assume A in DynSys X,G ; :: thesis: A ` in DynSys X,G
then X /\ A in G by Def9;
then A9: X \ (X /\ A) in G by Th22, XBOOLE_1:17;
X \ (X /\ A) = X /\ ((X /\ A) ` ) by SUBSET_1:32
.= X /\ ((X ` ) \/ (A ` )) by XBOOLE_1:54
.= (X /\ (X ` )) \/ (X /\ (A ` )) by XBOOLE_1:23
.= X /\ (A ` ) by A8 ;
hence A ` in DynSys X,G by A9, Def9; :: thesis: verum

end;

( {} /\ X = {} & {} in G ) by Def7;
then {} in DynSys X,G by Def9;
hence DynSys X,G is Dynkin_System of Omega by A1, A7, Def7; :: thesis: verum