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 :: thesis: for x being object st x in rng (seqIntersection (X1,f)) holds
x in G

let x be object ; :: 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, Def1;
hence x in G by A2, A5, Def7; :: thesis: verum

end;

then A6: rng (seqIntersection (X1,f)) c= G ;
seqIntersection (X,f) is disjoint_valued by A3, Th8;
then Union (seqIntersection (X1,f)) in G by A6, Def5;
then X /\ (Union f) in G by Th9;
hence Union f in DynSys (X,G) by Def7; :: 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 Def7;
then A9: X \ (X /\ A) in G by Th18, XBOOLE_1:17;
X \ (X /\ A) = X /\ ((X /\ A) `) by SUBSET_1:13
.= 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, Def7; :: thesis: verum

end;

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