( {} /\ X = {} & {} in G ) by Def7;
then A1: {} in DynSys X,G by Def9;
A2: 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

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 A3: ( rng f c= DynSys X,G & f is disjoint_valued ) ; :: thesis: Union f in DynSys X,G
reconsider X1 = X as Subset of Omega ;
A4: seqIntersection X,f is disjoint_valued by A3, Th12;

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
A5: x = (seqIntersection X1,f) . n by Th1;
A6: x = X /\ (f . n) by A5, Def2;
f . n in rng f by Th1;
hence x in G by A3, A6, Def9; :: thesis: verum

end;

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

end;

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 )
assume A in DynSys X,G ; :: thesis: A ` in DynSys X,G
then X /\ A in G by Def9;
then A7: X \ (X /\ A) in G by Th22, XBOOLE_1:17;
X misses X ` by XBOOLE_1:79;
then A8: X /\ (X ` ) = {} by XBOOLE_0:def 7;
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 A7, Def9; :: thesis: verum

end;

hence DynSys X,G is Dynkin_System of Omega by A1, A2, Def7; :: thesis: verum