:: DYNKIN semantic presentation

begin


theorem Th1: :: DYNKIN:1
for Omega being non empty set
for f being SetSequence of Omega
for x being set holds
( x in rng f iff ex n being Element of NAT st f . n = x )
proof
let Omega be non empty set ; ::_thesis: for f being SetSequence of Omega
for x being set holds
( x in rng f iff ex n being Element of NAT st f . n = x )
let f be SetSequence of Omega; ::_thesis: for x being set holds
( x in rng f iff ex n being Element of NAT st f . n = x )
let x be set ; ::_thesis: ( x in rng f iff ex n being Element of NAT st f . n = x )
A1: now__::_thesis:_(_x_in_rng_f_implies_ex_n_being_Element_of_NAT_st_f_._n_=_x_)
assume  x in rng f ; ::_thesis: ex n being Element of NAT st f . n = x
then consider z being set  such that
A2: z in dom f and
A3: x = f . z by FUNCT_1:def_3;
reconsider n = z as Element of NAT by A2, FUNCT_2:def_1;
take n = n; ::_thesis: f . n = x
thus  f . n = x by A3; ::_thesis: verum
end;
 dom f = NAT by FUNCT_2:def_1;
hence  ( x in rng f iff ex n being Element of NAT st f . n = x ) by A1, FUNCT_1:def_3; ::_thesis: verum
end;

theorem Th2: :: DYNKIN:2
for n being Element of NAT holds n is finite
proof
defpred S1[ Element of NAT ] means $1 is finite ;
A1: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  S1[n] ; ::_thesis: S1[n + 1]
then  succ n is finite ;
hence  S1[n + 1] by NAT_1:38; ::_thesis: verum
end;
A2: S1[ 0 ] ;
thus  for n being Element of NAT holds S1[n] from NAT_1:sch_1(A2, A1); ::_thesis: verum
end;

registration
let n be Element of NAT ;
cluster Segm n ->  finite ;
coherence
 Segm n is finite by Th2;
end;

Lm1:  for X being non empty set
for a, b, c being Element of X holds (a,b) followed_by c is Function of NAT,X
;

definition
let Omega be non empty set ;
let a, b, c be Subset of Omega;
:: original: followed_by
redefine func(a,b) followed_by c ->  SetSequence of Omega;
coherence
 (a,b) followed_by c is SetSequence of Omega
proof
thus  (a,b) followed_by c is SetSequence of Omega ; ::_thesis: verum
end;
end;

theorem Th3: :: DYNKIN:3
for a, b being set holds Union ((a,b) followed_by {}) = a \/ b
proof
let a, b be set ; ::_thesis: Union ((a,b) followed_by {}) = a \/ b
 rng ((a,b) followed_by {}) = {a,b,{}} by FUNCT_7:127;
hence  Union ((a,b) followed_by {}) = union {a,b} by MEASURE1:1
.= a \/ b by ZFMISC_1:75 ;
::_thesis: verum
end;

definition
let Omega be non empty set ;
let f be SetSequence of Omega;
let X be Subset of Omega;
func seqIntersection (X,f) ->  SetSequence of Omega means :Def1: :: DYNKIN:def 1
 for n being Element of NAT holds it . n = X /\ (f . n);
existence
 ex b1 being SetSequence of Omega st
for n being Element of NAT holds b1 . n = X /\ (f . n)
proof
deffunc H1( Element of NAT ) ->  Element of bool Omega = X /\ (f . $1);
consider g being Function of NAT,(bool Omega) such that
A1: for x being Element of NAT holds g . x = H1(x) from FUNCT_2:sch_4();
take  g ; ::_thesis: for n being Element of NAT holds g . n = X /\ (f . n)
let n be Element of NAT ; ::_thesis: g . n = X /\ (f . n)
thus  g . n = X /\ (f . n) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being SetSequence of Omega st ( for n being Element of NAT holds b1 . n = X /\ (f . n) ) & ( for n being Element of NAT holds b2 . n = X /\ (f . n) ) holds
b1 = b2
proof
let i1, i2 be SetSequence of Omega; ::_thesis: ( ( for n being Element of NAT holds i1 . n = X /\ (f . n) ) & ( for n being Element of NAT holds i2 . n = X /\ (f . n) ) implies i1 = i2 )
assume A2: for n being Element of NAT holds i1 . n = X /\ (f . n) ; ::_thesis: ( ex n being Element of NAT st not i2 . n = X /\ (f . n) or i1 = i2 )
assume A3: for n being Element of NAT holds i2 . n = X /\ (f . n) ; ::_thesis: i1 = i2
now__::_thesis:_for_n_being_Element_of_NAT_holds_i1_._n_=_i2_._n
let n be Element of NAT ; ::_thesis: i1 . n = i2 . n
 i1 . n = X /\ (f . n) by A2;
hence  i1 . n = i2 . n by A3; ::_thesis: verum
end;
hence  i1 = i2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines seqIntersection DYNKIN:def_1_:_
 for Omega being non empty set
for f being SetSequence of Omega
for X being Subset of Omega
for b4 being SetSequence of Omega holds
( b4 = seqIntersection (X,f) iff for n being Element of NAT holds b4 . n = X /\ (f . n) );

begin

definition
let Omega be non empty set ;
let f be SetSequence of Omega;
:: original: disjoint_valued
redefine attrf is disjoint_valued  means :Def2: :: DYNKIN:def 2
 for n, m being Element of NAT st n < m holds
f . n misses f . m;
compatibility
 ( f is disjoint_valued iff for n, m being Element of NAT st n < m holds
f . n misses f . m )
proof
thus  ( f is disjoint_valued implies for n, m being Element of NAT st n < m holds
f . n misses f . m ) by PROB_2:def_2; ::_thesis: ( ( for n, m being Element of NAT st n < m holds
f . n misses f . m ) implies f is disjoint_valued )
assume A1: for n, m being Element of NAT st n < m holds
f . n misses f . m ; ::_thesis: f is disjoint_valued
now__::_thesis:_for_x,_y_being_set_st_x_<>_y_holds_
f_._x_misses_f_._y
let x, y be set ; ::_thesis: ( x <> y implies f . b1 misses f . b2 )
assume A2: x <> y ; ::_thesis: f . b1 misses f . b2
percases ( ( x in dom f & y in dom f ) or not x in dom f or not y in dom f ) ;
suppose ( x in dom f & y in dom f ) ; ::_thesis: f . b1 misses f . b2
then reconsider n = x, m = y as Element of NAT by FUNCT_2:def_1;
 ( n < m or n > m ) by A2, XXREAL_0:1;
hence  f . x misses f . y by A1; ::_thesis: verum
end;
suppose ( not x in dom f or not y in dom f ) ; ::_thesis: f . b1 misses f . b2
then  ( f . x = {} or f . y = {} ) by FUNCT_1:def_2;
hence  f . x misses f . y by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
hence  f is disjoint_valued by PROB_2:def_2; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines disjoint_valued DYNKIN:def_2_:_
 for Omega being non empty set
for f being SetSequence of Omega holds
( f is disjoint_valued iff for n, m being Element of NAT st n < m holds
f . n misses f . m );

theorem Th4: :: DYNKIN:4
for Y being non empty set
for x being set holds
( x c= meet Y iff for y being Element of Y holds x c= y )
proof
let Y be non empty set ; ::_thesis: for x being set holds
( x c= meet Y iff for y being Element of Y holds x c= y )
let x be set ; ::_thesis: ( x c= meet Y iff for y being Element of Y holds x c= y )
hereby  ::_thesis: ( ( for y being Element of Y holds x c= y ) implies x c= meet Y )
assume A1: x c= meet Y ; ::_thesis: for y being Element of Y holds x c= y
let y be Element of Y; ::_thesis: x c= y
 for z being set st z in x holds
z in y by A1, SETFAM_1:def_1;
hence  x c= y by TARSKI:def_3; ::_thesis: verum
end;
assume A2: for y being Element of Y holds x c= y ; ::_thesis: x c= meet Y
 for z being set st z in x holds
z in meet Y
proof
let z be set ; ::_thesis: ( z in x implies z in meet Y )
assume A3: z in x ; ::_thesis: z in meet Y
now__::_thesis:_for_u_being_set_st_u_in_Y_holds_
z_in_u
let u be set ; ::_thesis: ( u in Y implies z in u )
assume  u in Y ; ::_thesis: z in u
then  x c= u by A2;
hence  z in u by A3; ::_thesis: verum
end;
hence  z in meet Y by SETFAM_1:def_1; ::_thesis: verum
end;
hence  x c= meet Y by TARSKI:def_3; ::_thesis: verum
end;

notation
let x be set ;
synonym  intersection_stable x for  cap-closed ;
end;

definition
let Omega be non empty set ;
let f be SetSequence of Omega;
let n be Nat;
func disjointify (f,n) ->  Subset of Omega equals :: DYNKIN:def 3
(f . n) \ (union (rng (f | n)));
coherence
 (f . n) \ (union (rng (f | n))) is Subset of Omega ;
end;

:: deftheorem  defines disjointify DYNKIN:def_3_:_
 for Omega being non empty set
for f being SetSequence of Omega
for n being Nat holds disjointify (f,n) = (f . n) \ (union (rng (f | n)));

definition
let Omega be non empty set ;
let g be SetSequence of Omega;
func disjointify g ->  SetSequence of Omega means :Def4: :: DYNKIN:def 4
 for n being Nat holds it . n = disjointify (g,n);
existence
 ex b1 being SetSequence of Omega st
for n being Nat holds b1 . n = disjointify (g,n)
proof
deffunc H1( Nat) ->  Subset of Omega = disjointify (g,$1);
consider f being Function of NAT,(bool Omega) such that
A1: for x being Element of NAT holds f . x = H1(x) from FUNCT_2:sch_4();
take  f ; ::_thesis: for n being Nat holds f . n = disjointify (g,n)
let n be Nat; ::_thesis: f . n = disjointify (g,n)
 n in NAT by ORDINAL1:def_12;
hence  f . n = disjointify (g,n) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being SetSequence of Omega st ( for n being Nat holds b1 . n = disjointify (g,n) ) & ( for n being Nat holds b2 . n = disjointify (g,n) ) holds
b1 = b2
proof
let i1, i2 be SetSequence of Omega; ::_thesis: ( ( for n being Nat holds i1 . n = disjointify (g,n) ) & ( for n being Nat holds i2 . n = disjointify (g,n) ) implies i1 = i2 )
assume A2: for n being Nat holds i1 . n = disjointify (g,n) ; ::_thesis: ( ex n being Nat st not i2 . n = disjointify (g,n) or i1 = i2 )
assume A3: for n being Nat holds i2 . n = disjointify (g,n) ; ::_thesis: i1 = i2
now__::_thesis:_for_n_being_Element_of_NAT_holds_i1_._n_=_i2_._n
let n be Element of NAT ; ::_thesis: i1 . n = i2 . n
 i1 . n = disjointify (g,n) by A2;
hence  i1 . n = i2 . n by A3; ::_thesis: verum
end;
hence  i1 = i2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines disjointify DYNKIN:def_4_:_
 for Omega being non empty set
for g, b3 being SetSequence of Omega holds
( b3 = disjointify g iff for n being Nat holds b3 . n = disjointify (g,n) );

theorem Th5: :: DYNKIN:5
for Omega being non empty set
for f being SetSequence of Omega
for n being Nat holds (disjointify f) . n = (f . n) \ (union (rng (f | n)))
proof
let Omega be non empty set ; ::_thesis: for f being SetSequence of Omega
for n being Nat holds (disjointify f) . n = (f . n) \ (union (rng (f | n)))
let f be SetSequence of Omega; ::_thesis: for n being Nat holds (disjointify f) . n = (f . n) \ (union (rng (f | n)))
let n be Nat; ::_thesis: (disjointify f) . n = (f . n) \ (union (rng (f | n)))
 (disjointify f) . n = disjointify (f,n) by Def4;
hence  (disjointify f) . n = (f . n) \ (union (rng (f | n))) ; ::_thesis: verum
end;

theorem Th6: :: DYNKIN:6
for Omega being non empty set
for f being SetSequence of Omega holds disjointify f is V56()
proof
let Omega be non empty set ; ::_thesis: for f being SetSequence of Omega holds disjointify f is V56()
let f be SetSequence of Omega; ::_thesis: disjointify f is V56()
now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_<_m_holds_
(disjointify_f)_._n_misses_(disjointify_f)_._m
let n, m be Element of NAT ; ::_thesis: ( n < m implies (disjointify f) . n misses (disjointify f) . m )
assume  n < m ; ::_thesis: (disjointify f) . n misses (disjointify f) . m
then A1: n in m by NAT_1:44;
 dom f = NAT by FUNCT_2:def_1;
then  dom (f | m) = m /\ NAT by RELAT_1:61;
then  n in dom (f | m) by A1, XBOOLE_0:def_4;
then A2: (f | m) . n in rng (f | m) by FUNCT_1:def_3;
 (f | m) . n = f . n by A1, FUNCT_1:49;
then  f . n misses (f . m) \ (union (rng (f | m))) by A2, XBOOLE_1:85, ZFMISC_1:74;
then A3: f . n misses (disjointify f) . m by Th5;
 (f . n) \ (union (rng (f | n))) c= f . n by XBOOLE_1:36;
then  (disjointify f) . n c= f . n by Th5;
hence  (disjointify f) . n misses (disjointify f) . m by A3, XBOOLE_1:63; ::_thesis: verum
end;
hence  disjointify f is V56() by Def2; ::_thesis: verum
end;

theorem Th7: :: DYNKIN:7
for Omega being non empty set
for f being SetSequence of Omega holds union (rng (disjointify f)) = union (rng f)
proof
let Omega be non empty set ; ::_thesis: for f being SetSequence of Omega holds union (rng (disjointify f)) = union (rng f)
let f be SetSequence of Omega; ::_thesis: union (rng (disjointify f)) = union (rng f)
A1: dom f = NAT by FUNCT_2:def_1;
A2: dom (disjointify f) = NAT by FUNCT_2:def_1;
now__::_thesis:_for_x_being_set_st_x_in_union_(rng_f)_holds_
x_in_union_(rng_(disjointify_f))
let x be set ; ::_thesis: ( x in union (rng f) implies x in union (rng (disjointify f)) )
defpred S1[ Nat] means x in f . $1;
assume  x in union (rng f) ; ::_thesis: x in union (rng (disjointify f))
then consider y being set  such that
A3: x in y and
A4: y in rng f by TARSKI:def_4;
consider z being set  such that
A5: z in dom f and
A6: y = f . z by A4, FUNCT_1:def_3;
reconsider n = z as Element of NAT by A5, FUNCT_2:def_1;
A7: ex k being Nat st S1[k]
proof
take  n ; ::_thesis: S1[n]
thus  S1[n] by A3, A6; ::_thesis: verum
end;
consider k being Nat such that
A8: ( S1[k] & ( for m being Nat st S1[m] holds
k <= m ) ) from NAT_1:sch_5(A7);
now__::_thesis:_not_x_in_union_(rng_(f_|_k))
assume  x in union (rng (f | k)) ; ::_thesis: contradiction
then consider y being set  such that
A9: x in y and
A10: y in rng (f | k) by TARSKI:def_4;
consider z being set  such that
A11: z in dom (f | k) and
A12: y = (f | k) . z by A10, FUNCT_1:def_3;
 dom (f | k) c= NAT by A1, RELAT_1:60;
then reconsider n = z as Element of NAT by A11;
 dom (f | k) c= k by RELAT_1:58;
then  ( n < k & y = f . n ) by A11, A12, FUNCT_1:49, NAT_1:44;
hence  contradiction by A8, A9; ::_thesis: verum
end;
then  x in (f . k) \ (union (rng (f | k))) by A8, XBOOLE_0:def_5;
then A13: x in (disjointify f) . k by Th5;
 k in NAT by ORDINAL1:def_12;
then  (disjointify f) . k in rng (disjointify f) by A2, FUNCT_1:def_3;
hence  x in union (rng (disjointify f)) by A13, TARSKI:def_4; ::_thesis: verum
end;
then A14: union (rng f) c= union (rng (disjointify f)) by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_union_(rng_(disjointify_f))_holds_
x_in_union_(rng_f)
let x be set ; ::_thesis: ( x in union (rng (disjointify f)) implies x in union (rng f) )
assume  x in union (rng (disjointify f)) ; ::_thesis: x in union (rng f)
then consider y being set  such that
A15: x in y and
A16: y in rng (disjointify f) by TARSKI:def_4;
consider z being set  such that
A17: z in dom (disjointify f) and
A18: y = (disjointify f) . z by A16, FUNCT_1:def_3;
reconsider n = z as Element of NAT by A17, FUNCT_2:def_1;
A19: ( (f . n) \ (union (rng (f | n))) c= f . n & f . n in rng f ) by A1, FUNCT_1:def_3, XBOOLE_1:36;
 x in (f . n) \ (union (rng (f | n))) by A15, A18, Th5;
hence  x in union (rng f) by A19, TARSKI:def_4; ::_thesis: verum
end;
then  union (rng (disjointify f)) c= union (rng f) by TARSKI:def_3;
hence  union (rng (disjointify f)) = union (rng f) by A14, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th8: :: DYNKIN:8
for Omega being non empty set
for x, y being Subset of Omega st x misses y holds
(x,y) followed_by ({} Omega) is V56()
proof
let Omega be non empty set ; ::_thesis: for x, y being Subset of Omega st x misses y holds
(x,y) followed_by ({} Omega) is V56()
let x, y be Subset of Omega; ::_thesis: ( x misses y implies (x,y) followed_by ({} Omega) is V56() )
assume A1: x misses y ; ::_thesis: (x,y) followed_by ({} Omega) is V56()
reconsider r = (x,y) followed_by ({} Omega) as Function of NAT,(bool Omega) ;
now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_<_m_holds_
r_._n_misses_r_._m
let n, m be Element of NAT ; ::_thesis: ( n < m implies r . n misses r . m )
A2: ( m > 1 implies r . m = {} ) by FUNCT_7:124;
assume A3: n < m ; ::_thesis: r . n misses r . m
A4: now__::_thesis:_(_(_m_=_0_or_m_=_1_)_implies_(_n_=_0_&_m_=_1_)_)
assume A5: ( m = 0 or m = 1 ) ; ::_thesis: ( n = 0 & m = 1 )
 0 + 1 = 1 ;
then  n <= 0 by A3, A5, NAT_1:13;
hence  ( n = 0 & m = 1 ) by A3, A5, NAT_1:3; ::_thesis: verum
end;
 r . 0 = x by FUNCT_7:122;
hence  r . n misses r . m by A1, A4, A2, FUNCT_7:123, NAT_1:25, XBOOLE_1:65; ::_thesis: verum
end;
hence  (x,y) followed_by ({} Omega) is V56() by Def2; ::_thesis: verum
end;

theorem Th9: :: DYNKIN:9
for Omega being non empty set
for f being SetSequence of Omega st f is V56() holds
for X being Subset of Omega holds seqIntersection (X,f) is V56()
proof
let Omega be non empty set ; ::_thesis: for f being SetSequence of Omega st f is V56() holds
for X being Subset of Omega holds seqIntersection (X,f) is V56()
let f be SetSequence of Omega; ::_thesis: ( f is V56() implies for X being Subset of Omega holds seqIntersection (X,f) is V56() )
assume A1: f is V56() ; ::_thesis: for X being Subset of Omega holds seqIntersection (X,f) is V56()
let X be Subset of Omega; ::_thesis: seqIntersection (X,f) is V56()
 for n, m being Element of NAT st n < m holds
(seqIntersection (X,f)) . n misses (seqIntersection (X,f)) . m
proof
let n, m be Element of NAT ; ::_thesis: ( n < m implies (seqIntersection (X,f)) . n misses (seqIntersection (X,f)) . m )
assume  n < m ; ::_thesis: (seqIntersection (X,f)) . n misses (seqIntersection (X,f)) . m
then  f . n misses f . m by A1, PROB_2:def_2;
then A2: X /\ (f . n) misses f . m by XBOOLE_1:74;
 ( (seqIntersection (X,f)) . n = X /\ (f . n) & (seqIntersection (X,f)) . m = X /\ (f . m) ) by Def1;
hence  (seqIntersection (X,f)) . n misses (seqIntersection (X,f)) . m by A2, XBOOLE_1:74; ::_thesis: verum
end;
hence  seqIntersection (X,f) is V56() by Def2; ::_thesis: verum
end;

theorem Th10: :: DYNKIN:10
for Omega being non empty set
for f being SetSequence of Omega
for X being Subset of Omega holds X /\ (Union f) = Union (seqIntersection (X,f))
proof
let Omega be non empty set ; ::_thesis: for f being SetSequence of Omega
for X being Subset of Omega holds X /\ (Union f) = Union (seqIntersection (X,f))
let f be SetSequence of Omega; ::_thesis: for X being Subset of Omega holds X /\ (Union f) = Union (seqIntersection (X,f))
let X be Subset of Omega; ::_thesis: X /\ (Union f) = Union (seqIntersection (X,f))
A1: dom f = NAT by FUNCT_2:def_1;
now__::_thesis:_for_z_being_set_st_z_in_Union_(seqIntersection_(X,f))_holds_
z_in_X_/\_(Union_f)
reconsider g = seqIntersection (X,f) as SetSequence of Omega ;
let z be set ; ::_thesis: ( z in Union (seqIntersection (X,f)) implies z in X /\ (Union f) )
assume  z in Union (seqIntersection (X,f)) ; ::_thesis: z in X /\ (Union f)
then consider u being set  such that
A2: z in u and
A3: u in rng g by TARSKI:def_4;
consider v being set  such that
A4: v in dom g and
A5: u = g . v by A3, FUNCT_1:def_3;
reconsider n = v as Element of NAT by A4, FUNCT_2:def_1;
A6: z in X /\ (f . n) by A2, A5, Def1;
then A7: z in X by XBOOLE_0:def_4;
A8: f . n in rng f by A1, FUNCT_1:def_3;
 z in f . n by A6, XBOOLE_0:def_4;
then  z in Union f by A8, TARSKI:def_4;
hence  z in X /\ (Union f) by A7, XBOOLE_0:def_4; ::_thesis: verum
end;
then A9: Union (seqIntersection (X,f)) c= X /\ (Union f) by TARSKI:def_3;
A10: dom (seqIntersection (X,f)) = NAT by FUNCT_2:def_1;
now__::_thesis:_for_z_being_set_st_z_in_X_/\_(Union_f)_holds_
z_in_Union_(seqIntersection_(X,f))
let z be set ; ::_thesis: ( z in X /\ (Union f) implies z in Union (seqIntersection (X,f)) )
assume A11: z in X /\ (Union f) ; ::_thesis: z in Union (seqIntersection (X,f))
then  z in union (rng f) by XBOOLE_0:def_4;
then consider u being set  such that
A12: z in u and
A13: u in rng f by TARSKI:def_4;
consider v being set  such that
A14: v in dom f and
A15: u = f . v by A13, FUNCT_1:def_3;
reconsider n = v as Element of NAT by A14, FUNCT_2:def_1;
 X /\ (f . n) = (seqIntersection (X,f)) . n by Def1;
then A16: X /\ (f . n) in rng (seqIntersection (X,f)) by A10, FUNCT_1:def_3;
 z in X by A11, XBOOLE_0:def_4;
then  z in X /\ (f . n) by A12, A15, XBOOLE_0:def_4;
hence  z in Union (seqIntersection (X,f)) by A16, TARSKI:def_4; ::_thesis: verum
end;
then  X /\ (Union f) c= Union (seqIntersection (X,f)) by TARSKI:def_3;
hence  X /\ (Union f) = Union (seqIntersection (X,f)) by A9, XBOOLE_0:def_10; ::_thesis: verum
end;

begin

definition
let Omega be non empty set ;
mode Dynkin_System of Omega ->  Subset-Family of Omega means :Def5: :: DYNKIN:def 5
( ( for f being SetSequence of Omega st rng f c= it & f is V56() holds
Union f in it ) & ( for X being Subset of Omega st X in it holds
X ` in it ) & {} in it );
existence
 ex b1 being Subset-Family of Omega st
( ( for f being SetSequence of Omega st rng f c= b1 & f is V56() holds
Union f in b1 ) & ( for X being Subset of Omega st X in b1 holds
X ` in b1 ) & {} in b1 )
proof
reconsider D = bool Omega as non empty Subset-Family of Omega ;
take  D ; ::_thesis: ( ( for f being SetSequence of Omega st rng f c= D & f is V56() holds
Union f in D ) & ( for X being Subset of Omega st X in D holds
X ` in D ) & {} in D )
 {} c= Omega by XBOOLE_1:2;
hence  ( ( for f being SetSequence of Omega st rng f c= D & f is V56() holds
Union f in D ) & ( for X being Subset of Omega st X in D holds
X ` in D ) & {} in D ) ; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines Dynkin_System DYNKIN:def_5_:_
 for Omega being non empty set
for b2 being Subset-Family of Omega holds
( b2 is Dynkin_System of Omega iff ( ( for f being SetSequence of Omega st rng f c= b2 & f is V56() holds
Union f in b2 ) & ( for X being Subset of Omega st X in b2 holds
X ` in b2 ) & {} in b2 ) );

registration
let Omega be non empty set ;
cluster  ->  non empty for Dynkin_System of Omega;
coherence
 for b1 being Dynkin_System of Omega holds not b1 is empty by Def5;
end;

theorem Th11: :: DYNKIN:11
for Omega being non empty set holds bool Omega is Dynkin_System of Omega
proof
let Omega be non empty set ; ::_thesis: bool Omega is Dynkin_System of Omega
A1: ( {} c= Omega & bool Omega c= bool Omega ) by XBOOLE_1:2;
 ( ( for f being SetSequence of Omega st rng f c= bool Omega & f is V56() holds
Union f in bool Omega ) & ( for X being Subset of Omega st X in bool Omega holds
X ` in bool Omega ) ) ;
hence  bool Omega is Dynkin_System of Omega by A1, Def5; ::_thesis: verum
end;

theorem Th12: :: DYNKIN:12
for F, Omega being non empty set st ( for Y being set st Y in F holds
Y is Dynkin_System of Omega ) holds
meet F is Dynkin_System of Omega
proof
let F, Omega be non empty set ; ::_thesis: ( ( for Y being set st Y in F holds
Y is Dynkin_System of Omega ) implies meet F is Dynkin_System of Omega )
assume A1: for Y being set st Y in F holds
Y is Dynkin_System of Omega ; ::_thesis: meet F is Dynkin_System of Omega
now__::_thesis:_for_Y_being_set_st_Y_in_F_holds_
{}_in_Y
let Y be set ; ::_thesis: ( Y in F implies {} in Y )
assume  Y in F ; ::_thesis: {} in Y
then  Y is Dynkin_System of Omega by A1;
hence  {} in Y by Def5; ::_thesis: verum
end;
then A2: {} in meet F by SETFAM_1:def_1;
A3: now__::_thesis:_for_f_being_SetSequence_of_Omega_st_rng_f_c=_meet_F_&_f_is_V56()_holds_
Union_f_in_meet_F
let f be SetSequence of Omega; ::_thesis: ( rng f c= meet F & f is V56() implies Union f in meet F )
assume that
A4: rng f c= meet F and
A5: f is V56() ; ::_thesis: Union f in meet F
now__::_thesis:_for_Y_being_set_st_Y_in_F_holds_
Union_f_in_Y
let Y be set ; ::_thesis: ( Y in F implies Union f in Y )
assume A6: Y in F ; ::_thesis: Union f in Y
 meet F c= Y by A6, SETFAM_1:3;
then A7: rng f c= Y by A4, XBOOLE_1:1;
 Y is Dynkin_System of Omega by A1, A6;
hence  Union f in Y by A5, A7, Def5; ::_thesis: verum
end;
hence  Union f in meet F by SETFAM_1:def_1; ::_thesis: verum
end;
A8: now__::_thesis:_for_X_being_Subset_of_Omega_st_X_in_meet_F_holds_
X_`_in_meet_F
let X be Subset of Omega; ::_thesis: ( X in meet F implies X ` in meet F )
assume A9: X in meet F ; ::_thesis: X ` in meet F
 for Y being set st Y in F holds
X ` in Y
proof
let Y be set ; ::_thesis: ( Y in F implies X ` in Y )
assume  Y in F ; ::_thesis: X ` in Y
then  ( Y is Dynkin_System of Omega & meet F c= Y ) by A1, SETFAM_1:3;
hence  X ` in Y by A9, Def5; ::_thesis: verum
end;
hence  X ` in meet F by SETFAM_1:def_1; ::_thesis: verum
end;
set Y = the Element of F;
A10: meet F c= the Element of F by SETFAM_1:3;
 the Element of F is Dynkin_System of Omega by A1;
then  meet F is Subset-Family of Omega by A10, XBOOLE_1:1;
hence  meet F is Dynkin_System of Omega by A3, A8, A2, Def5; ::_thesis: verum
end;

theorem Th13: :: DYNKIN:13
for Omega being non empty set
for A, B being Subset of Omega
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable & A in D & B in D holds
A \ B in D
proof
let Omega be non empty set ; ::_thesis: for A, B being Subset of Omega
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable & A in D & B in D holds
A \ B in D
let A, B be Subset of Omega; ::_thesis: for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable & A in D & B in D holds
A \ B in D
let D be non empty Subset-Family of Omega; ::_thesis: ( D is Dynkin_System of Omega & D is intersection_stable & A in D & B in D implies A \ B in D )
assume that
A1: D is Dynkin_System of Omega and
A2: D is intersection_stable ; ::_thesis: ( not A in D or not B in D or A \ B in D )
assume that
A3: A in D and
A4: B in D ; ::_thesis: A \ B in D
 B ` in D by A1, A4, Def5;
then  A /\ (B `) in D by A2, A3, FINSUB_1:def_2;
hence  A \ B in D by SUBSET_1:13; ::_thesis: verum
end;

theorem Th14: :: DYNKIN:14
for Omega being non empty set
for A, B being Subset of Omega
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable & A in D & B in D holds
A \/ B in D
proof
let Omega be non empty set ; ::_thesis: for A, B being Subset of Omega
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable & A in D & B in D holds
A \/ B in D
let A, B be Subset of Omega; ::_thesis: for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable & A in D & B in D holds
A \/ B in D
let D be non empty Subset-Family of Omega; ::_thesis: ( D is Dynkin_System of Omega & D is intersection_stable & A in D & B in D implies A \/ B in D )
assume that
A1: D is Dynkin_System of Omega and
A2: D is intersection_stable ; ::_thesis: ( not A in D or not B in D or A \/ B in D )
assume  ( A in D & B in D ) ; ::_thesis: A \/ B in D
then  ( A ` in D & B ` in D ) by A1, Def5;
then  (A `) /\ (B `) in D by A2, FINSUB_1:def_2;
then  (A \/ B) ` in D by XBOOLE_1:53;
then  ((A \/ B) `) ` in D by A1, Def5;
hence  A \/ B in D ; ::_thesis: verum
end;

theorem Th15: :: DYNKIN:15
for Omega being non empty set
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds
for x being finite set st x c= D holds
union x in D
proof
let Omega be non empty set ; ::_thesis: for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds
for x being finite set st x c= D holds
union x in D
let D be non empty Subset-Family of Omega; ::_thesis: ( D is Dynkin_System of Omega & D is intersection_stable implies for x being finite set st x c= D holds
union x in D )
assume that
A1: D is Dynkin_System of Omega and
A2: D is intersection_stable ; ::_thesis: for x being finite set st x c= D holds
union x in D
defpred S1[ set ] means  union $1 in D;
let x be finite set ; ::_thesis: ( x c= D implies union x in D )
assume A3: x c= D ; ::_thesis: union x in D
A4: for y, b being set st y in x & b c= x & S1[b] holds
S1[b \/ {y}]
proof
let y, b be set ; ::_thesis: ( y in x & b c= x & S1[b] implies S1[b \/ {y}] )
assume that
A5: y in x and
 b c= x and
A6: union b in D ; ::_thesis: S1[b \/ {y}]
 y in D by A3, A5;
then reconsider y1 = y as Subset of Omega ;
reconsider unionb = union b as Subset of Omega by A6;
 ( union {y} = y & unionb \/ y1 in D ) by A1, A2, A3, A5, A6, Th14, ZFMISC_1:25;
hence  S1[b \/ {y}] by ZFMISC_1:78; ::_thesis: verum
end;
A7: x is finite ;
A8: S1[ {} ] by A1, Def5, ZFMISC_1:2;
thus  S1[x] from FINSET_1:sch_2(A7, A8, A4); ::_thesis: verum
end;

theorem Th16: :: DYNKIN:16
for Omega being non empty set
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds
for f being SetSequence of Omega st rng f c= D holds
rng (disjointify f) c= D
proof
let Omega be non empty set ; ::_thesis: for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds
for f being SetSequence of Omega st rng f c= D holds
rng (disjointify f) c= D
let D be non empty Subset-Family of Omega; ::_thesis: ( D is Dynkin_System of Omega & D is intersection_stable implies for f being SetSequence of Omega st rng f c= D holds
rng (disjointify f) c= D )
assume A1: ( D is Dynkin_System of Omega & D is intersection_stable ) ; ::_thesis: for f being SetSequence of Omega st rng f c= D holds
rng (disjointify f) c= D
let f be SetSequence of Omega; ::_thesis: ( rng f c= D implies rng (disjointify f) c= D )
assume A2: rng f c= D ; ::_thesis: rng (disjointify f) c= D
A3: for n being Element of NAT holds (disjointify f) . n in D
proof
let n be Element of NAT ; ::_thesis: (disjointify f) . n in D
A4: rng (f | n) c= rng f by RELAT_1:70;
 ( dom (f | n) c= Segm n & rng f is Subset-Family of Omega ) by RELAT_1:58, RELAT_1:def_19;
then  rng (f | n) is finite Subset-Family of Omega by A4, XBOOLE_1:1;
then A5: union (rng (f | n)) in D by A1, A2, A4, Th15, XBOOLE_1:1;
then reconsider urf = union (rng (f | n)) as Subset of Omega ;
 dom f = NAT by FUNCT_2:def_1;
then  f . n in rng f by FUNCT_1:def_3;
then  (f . n) \ urf in D by A1, A2, A5, Th13;
hence  (disjointify f) . n in D by Th5; ::_thesis: verum
end;
now__::_thesis:_for_y_being_set_st_y_in_rng_(disjointify_f)_holds_
y_in_D
let y be set ; ::_thesis: ( y in rng (disjointify f) implies y in D )
assume  y in rng (disjointify f) ; ::_thesis: y in D
then consider x being set  such that
A6: x in dom (disjointify f) and
A7: y = (disjointify f) . x by FUNCT_1:def_3;
reconsider n = x as Element of NAT by A6, FUNCT_2:def_1;
 y = (disjointify f) . n by A7;
hence  y in D by A3; ::_thesis: verum
end;
hence  rng (disjointify f) c= D by TARSKI:def_3; ::_thesis: verum
end;

theorem Th17: :: DYNKIN:17
for Omega being non empty set
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds
for f being SetSequence of Omega st rng f c= D holds
union (rng f) in D
proof
let Omega be non empty set ; ::_thesis: for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds
for f being SetSequence of Omega st rng f c= D holds
union (rng f) in D
let D be non empty Subset-Family of Omega; ::_thesis: ( D is Dynkin_System of Omega & D is intersection_stable implies for f being SetSequence of Omega st rng f c= D holds
union (rng f) in D )
assume that
A1: D is Dynkin_System of Omega and
A2: D is intersection_stable ; ::_thesis: for f being SetSequence of Omega st rng f c= D holds
union (rng f) in D
let f be SetSequence of Omega; ::_thesis: ( rng f c= D implies union (rng f) in D )
assume  rng f c= D ; ::_thesis: union (rng f) in D
then A3: rng (disjointify f) c= D by A1, A2, Th16;
 disjointify f is V56() by Th6;
then  Union (disjointify f) in D by A1, A3, Def5;
hence  union (rng f) in D by Th7; ::_thesis: verum
end;

theorem Th18: :: DYNKIN:18
for Omega being non empty set
for D being Dynkin_System of Omega
for x, y being Element of D st x misses y holds
x \/ y in D
proof
let Omega be non empty set ; ::_thesis: for D being Dynkin_System of Omega
for x, y being Element of D st x misses y holds
x \/ y in D
let D be Dynkin_System of Omega; ::_thesis: for x, y being Element of D st x misses y holds
x \/ y in D
reconsider e = {} as Element of D by Def5;
let x, y be Element of D; ::_thesis: ( x misses y implies x \/ y in D )
reconsider x1 = x as Subset of Omega ;
reconsider y1 = y as Subset of Omega ;
reconsider r = (x1,y1) followed_by ({} Omega) as SetSequence of Omega ;
 (x,y) followed_by e is Function of NAT,D by Lm1;
then A1: rng r c= D by RELAT_1:def_19;
assume  x misses y ; ::_thesis: x \/ y in D
then  r is V56() by Th8;
then  Union r in D by A1, Def5;
hence  x \/ y in D by Th3; ::_thesis: verum
end;

theorem Th19: :: DYNKIN:19
for Omega being non empty set
for D being Dynkin_System of Omega
for x, y being Element of D st x c= y holds
y \ x in D
proof
let Omega be non empty set ; ::_thesis: for D being Dynkin_System of Omega
for x, y being Element of D st x c= y holds
y \ x in D
let D be Dynkin_System of Omega; ::_thesis: for x, y being Element of D st x c= y holds
y \ x in D
let x, y be Element of D; ::_thesis: ( x c= y implies y \ x in D )
A1: (x \/ (y `)) ` = (x `) /\ ((y `) `) by XBOOLE_1:53
.= y \ x by SUBSET_1:13 ;
assume  x c= y ; ::_thesis: y \ x in D
then  x c= (y `) ` ;
then A2: x misses y ` by SUBSET_1:23;
 y ` in D by Def5;
then  x \/ (y `) in D by A2, Th18;
hence  y \ x in D by A1, Def5; ::_thesis: verum
end;

begin

theorem Th20: :: DYNKIN:20
for Omega being non empty set
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds
D is SigmaField of Omega
proof
let Omega be non empty set ; ::_thesis: for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds
D is SigmaField of Omega
let D be non empty Subset-Family of Omega; ::_thesis: ( D is Dynkin_System of Omega & D is intersection_stable implies D is SigmaField of Omega )
assume that
A1: D is Dynkin_System of Omega and
A2: D is intersection_stable ; ::_thesis: D is SigmaField of Omega
A3: for f being SetSequence of Omega st rng f c= D holds
Intersection f in D
proof
let f be SetSequence of Omega; ::_thesis: ( rng f c= D implies Intersection f in D )
assume A4: rng f c= D ; ::_thesis: Intersection f in D
A5: for n being Element of NAT holds (f . n) ` in D
proof
let n be Element of NAT ; ::_thesis: (f . n) ` in D
 f . n in rng f by NAT_1:51;
hence  (f . n) ` in D by A1, A4, Def5; ::_thesis: verum
end;
A6: for n being Element of NAT holds (Complement f) . n in D
proof
let n be Element of NAT ; ::_thesis: (Complement f) . n in D
 (Complement f) . n = (f . n) ` by PROB_1:def_2;
hence  (Complement f) . n in D by A5; ::_thesis: verum
end;
 for x being set st x in rng (Complement f) holds
x in D
proof
let x be set ; ::_thesis: ( x in rng (Complement f) implies x in D )
assume  x in rng (Complement f) ; ::_thesis: x in D
then consider z being set  such that
A7: z in dom (Complement f) and
A8: x = (Complement f) . z by FUNCT_1:def_3;
reconsider n = z as Element of NAT by A7, FUNCT_2:def_1;
 x = (Complement f) . n by A8;
hence  x in D by A6; ::_thesis: verum
end;
then  rng (Complement f) c= D by TARSKI:def_3;
then  Union (Complement f) in D by A1, A2, Th17;
then  (Union (Complement f)) ` in D by A1, Def5;
hence  Intersection f in D by PROB_1:def_3; ::_thesis: verum
end;
 for X being Subset of Omega st X in D holds
X ` in D by A1, Def5;
hence  D is SigmaField of Omega by A3, PROB_1:15; ::_thesis: verum
end;

definition
let Omega be non empty set ;
let E be Subset-Family of Omega;
func generated_Dynkin_System E ->  Dynkin_System of Omega means :Def6: :: DYNKIN:def 6
( E c= it & ( for D being Dynkin_System of Omega st E c= D holds
it c= D ) );
existence
 ex b1 being Dynkin_System of Omega st
( E c= b1 & ( for D being Dynkin_System of Omega st E c= D holds
b1 c= D ) )
proof
defpred S1[ set ] means ( $1 is Dynkin_System of Omega & E c= $1 );
consider Y being set  such that
A1: for x being set holds
( x in Y iff ( x in bool (bool Omega) & S1[x] ) ) from XBOOLE_0:sch_1();
 bool Omega is Dynkin_System of Omega by Th11;
then reconsider Y = Y as non empty set by A1;
 for z being set st z in Y holds
z is Dynkin_System of Omega by A1;
then reconsider I = meet Y as Dynkin_System of Omega by Th12;
take  I ; ::_thesis: ( E c= I & ( for D being Dynkin_System of Omega st E c= D holds
I c= D ) )
 for y being Element of Y holds E c= y by A1;
hence  E c= I by Th4; ::_thesis: for D being Dynkin_System of Omega st E c= D holds
I c= D
let D be Dynkin_System of Omega; ::_thesis: ( E c= D implies I c= D )
assume  E c= D ; ::_thesis: I c= D
then  D in Y by A1;
hence  I c= D by SETFAM_1:3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Dynkin_System of Omega st E c= b1 & ( for D being Dynkin_System of Omega st E c= D holds
b1 c= D ) & E c= b2 & ( for D being Dynkin_System of Omega st E c= D holds
b2 c= D ) holds
b1 = b2
proof
let I1, I2 be Dynkin_System of Omega; ::_thesis: ( E c= I1 & ( for D being Dynkin_System of Omega st E c= D holds
I1 c= D ) & E c= I2 & ( for D being Dynkin_System of Omega st E c= D holds
I2 c= D ) implies I1 = I2 )
assume A2: ( E c= I1 & ( for D being Dynkin_System of Omega st E c= D holds
I1 c= D ) ) ; ::_thesis: ( not E c= I2 or ex D being Dynkin_System of Omega st
( E c= D & not I2 c= D ) or I1 = I2 )
assume  ( E c= I2 & ( for D being Dynkin_System of Omega st E c= D holds
I2 c= D ) ) ; ::_thesis: I1 = I2
then  ( I1 c= I2 & I2 c= I1 ) by A2;
hence  I1 = I2 by XBOOLE_0:def_10; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines generated_Dynkin_System DYNKIN:def_6_:_
 for Omega being non empty set
for E being Subset-Family of Omega
for b3 being Dynkin_System of Omega holds
( b3 = generated_Dynkin_System E iff ( E c= b3 & ( for D being Dynkin_System of Omega st E c= D holds
b3 c= D ) ) );

definition
let Omega be non empty set ;
let G be set ;
let X be Subset of Omega;
func DynSys (X,G) ->  Subset-Family of Omega means :Def7: :: DYNKIN:def 7
 for A being Subset of Omega holds
( A in it iff A /\ X in G );
existence
 ex b1 being Subset-Family of Omega st
for A being Subset of Omega holds
( A in b1 iff A /\ X in G )
proof
defpred S1[ set ] means $1 /\ X in G;
consider I being set  such that
A1: for x being set holds
( x in I iff ( x in bool Omega & S1[x] ) ) from XBOOLE_0:sch_1();
 for x being set st x in I holds
x in bool Omega by A1;
then reconsider I = I as Subset-Family of Omega by TARSKI:def_3;
take  I ; ::_thesis: for A being Subset of Omega holds
( A in I iff A /\ X in G )
let A be Subset of Omega; ::_thesis: ( A in I iff A /\ X in G )
thus  ( A in I iff A /\ X in G ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset-Family of Omega st ( for A being Subset of Omega holds
( A in b1 iff A /\ X in G ) ) & ( for A being Subset of Omega holds
( A in b2 iff A /\ X in G ) ) holds
b1 = b2
proof
let I1, I2 be Subset-Family of Omega; ::_thesis: ( ( for A being Subset of Omega holds
( A in I1 iff A /\ X in G ) ) & ( for A being Subset of Omega holds
( A in I2 iff A /\ X in G ) ) implies I1 = I2 )
assume A2: for A being Subset of Omega holds
( A in I1 iff A /\ X in G ) ; ::_thesis: ( ex A being Subset of Omega st
( ( A in I2 implies A /\ X in G ) implies ( A /\ X in G & not A in I2 ) ) or I1 = I2 )
assume A3: for A being Subset of Omega holds
( A in I2 iff A /\ X in G ) ; ::_thesis: I1 = I2
now__::_thesis:_for_A_being_Subset_of_Omega_holds_
(_A_in_I1_iff_A_in_I2_)
let A be Subset of Omega; ::_thesis: ( A in I1 iff A in I2 )
 ( A in I1 iff A /\ X in G ) by A2;
hence  ( A in I1 iff A in I2 ) by A3; ::_thesis: verum
end;
hence  I1 = I2 by SUBSET_1:3; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines DynSys DYNKIN:def_7_:_
 for Omega being non empty set
for G being set
for X being Subset of Omega
for b4 being Subset-Family of Omega holds
( b4 = DynSys (X,G) iff for A being Subset of Omega holds
( A in b4 iff A /\ X in G ) );

definition
let Omega be non empty set ;
let G be Dynkin_System of Omega;
let X be Element of G;
:: original: DynSys
redefine func DynSys (X,G) ->  Dynkin_System of Omega;
coherence
 DynSys (X,G) is Dynkin_System of Omega
proof
A1: for f being SetSequence of Omega st rng f c= DynSys (X,G) & f is V56() 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 V56() implies Union f in DynSys (X,G) )
assume that
A2: rng f c= DynSys (X,G) and
A3: f is V56() ; ::_thesis: Union f in DynSys (X,G)
now__::_thesis:_for_x_being_set_st_x_in_rng_(seqIntersection_(X1,f))_holds_
x_in_G
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, Def1;
hence  x in G by A2, A5, Def7; ::_thesis: verum
end;
then A6: rng (seqIntersection (X1,f)) c= G by TARSKI:def_3;
 seqIntersection (X,f) is V56() by A3, Th9;
then  Union (seqIntersection (X1,f)) in G by A6, Def5;
then  X /\ (Union f) in G by Th10;
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 Th19, 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
end;
end;

theorem Th21: :: DYNKIN:21
for Omega being non empty set
for E being Subset-Family of Omega
for X, Y being Subset of Omega st X in E & Y in generated_Dynkin_System E & E is intersection_stable holds
X /\ Y in generated_Dynkin_System E
proof
let Omega be non empty set ; ::_thesis: for E being Subset-Family of Omega
for X, Y being Subset of Omega st X in E & Y in generated_Dynkin_System E & E is intersection_stable holds
X /\ Y in generated_Dynkin_System E
let E be Subset-Family of Omega; ::_thesis: for X, Y being Subset of Omega st X in E & Y in generated_Dynkin_System E & E is intersection_stable holds
X /\ Y in generated_Dynkin_System E
let X, Y be Subset of Omega; ::_thesis: ( X in E & Y in generated_Dynkin_System E & E is intersection_stable implies X /\ Y in generated_Dynkin_System E )
assume that
A1: X in E and
A2: Y in generated_Dynkin_System E and
A3: E is intersection_stable ; ::_thesis: X /\ Y in generated_Dynkin_System E
reconsider G = generated_Dynkin_System E as Dynkin_System of Omega ;
 E c= generated_Dynkin_System E by Def6;
then reconsider X = X as Element of G by A1;
 for x being set st x in E holds
x in DynSys (X,G)
proof
let x be set ; ::_thesis: ( x in E implies x in DynSys (X,G) )
assume A4: x in E ; ::_thesis: x in DynSys (X,G)
then reconsider x = x as Subset of Omega ;
A5: E c= G by Def6;
 x /\ X in E by A1, A3, A4, FINSUB_1:def_2;
hence  x in DynSys (X,G) by A5, Def7; ::_thesis: verum
end;
then  E c= DynSys (X,G) by TARSKI:def_3;
then  generated_Dynkin_System E c= DynSys (X,G) by Def6;
hence  X /\ Y in generated_Dynkin_System E by A2, Def7; ::_thesis: verum
end;

theorem Th22: :: DYNKIN:22
for Omega being non empty set
for E being Subset-Family of Omega
for X, Y being Subset of Omega st X in generated_Dynkin_System E & Y in generated_Dynkin_System E & E is intersection_stable holds
X /\ Y in generated_Dynkin_System E
proof
let Omega be non empty set ; ::_thesis: for E being Subset-Family of Omega
for X, Y being Subset of Omega st X in generated_Dynkin_System E & Y in generated_Dynkin_System E & E is intersection_stable holds
X /\ Y in generated_Dynkin_System E
let E be Subset-Family of Omega; ::_thesis: for X, Y being Subset of Omega st X in generated_Dynkin_System E & Y in generated_Dynkin_System E & E is intersection_stable holds
X /\ Y in generated_Dynkin_System E
let X, Y be Subset of Omega; ::_thesis: ( X in generated_Dynkin_System E & Y in generated_Dynkin_System E & E is intersection_stable implies X /\ Y in generated_Dynkin_System E )
assume that
A1: X in generated_Dynkin_System E and
A2: Y in generated_Dynkin_System E and
A3: E is intersection_stable ; ::_thesis: X /\ Y in generated_Dynkin_System E
reconsider G = generated_Dynkin_System E as Dynkin_System of Omega ;
defpred S1[ set ] means  ex X being Element of G st $1 = DynSys (X,G);
consider h being set  such that
A4: for x being set holds
( x in h iff ( x in bool (bool Omega) & S1[x] ) ) from XBOOLE_0:sch_1();
A5: for Y being set st Y in h holds
Y is Dynkin_System of Omega
proof
let Y be set ; ::_thesis: ( Y in h implies Y is Dynkin_System of Omega )
assume  Y in h ; ::_thesis: Y is Dynkin_System of Omega
then  ex X being Element of G st Y = DynSys (X,G) by A4;
hence  Y is Dynkin_System of Omega ; ::_thesis: verum
end;
 not h is empty
proof
set X = the Element of G;
 DynSys ( the Element of G,G) in h by A4;
hence  not h is empty ; ::_thesis: verum
end;
then reconsider h = h as non empty set ;
 DynSys (X,G) in h by A1, A4;
then A6: meet h c= DynSys (X,G) by SETFAM_1:3;
 for x being set st x in E holds
x in meet h
proof
let x be set ; ::_thesis: ( x in E implies x in meet h )
assume A7: x in E ; ::_thesis: x in meet h
 for Y being set st Y in h holds
x in Y
proof
let Y be set ; ::_thesis: ( Y in h implies x in Y )
assume  Y in h ; ::_thesis: x in Y
then consider X being Element of G such that
A8: Y = DynSys (X,G) by A4;
 x /\ X in G by A3, A7, Th21;
hence  x in Y by A7, A8, Def7; ::_thesis: verum
end;
hence  x in meet h by SETFAM_1:def_1; ::_thesis: verum
end;
then A9: E c= meet h by TARSKI:def_3;
 meet h is Dynkin_System of Omega by A5, Th12;
then  G c= meet h by A9, Def6;
then  G c= DynSys (X,G) by A6, XBOOLE_1:1;
hence  X /\ Y in generated_Dynkin_System E by A2, Def7; ::_thesis: verum
end;

theorem Th23: :: DYNKIN:23
for Omega being non empty set
for E being Subset-Family of Omega st E is intersection_stable holds
generated_Dynkin_System E is intersection_stable
proof
let Omega be non empty set ; ::_thesis: for E being Subset-Family of Omega st E is intersection_stable holds
generated_Dynkin_System E is intersection_stable
let E be Subset-Family of Omega; ::_thesis: ( E is intersection_stable implies generated_Dynkin_System E is intersection_stable )
assume A1: E is intersection_stable ; ::_thesis: generated_Dynkin_System E is intersection_stable
reconsider G = generated_Dynkin_System E as Subset-Family of Omega ;
 for a, b being set st a in G & b in G holds
a /\ b in G by A1, Th22;
hence  generated_Dynkin_System E is intersection_stable by FINSUB_1:def_2; ::_thesis: verum
end;

theorem :: DYNKIN:24
for Omega being non empty set
for E being Subset-Family of Omega st E is intersection_stable holds
for D being Dynkin_System of Omega st E c= D holds
sigma E c= D
proof
let Omega be non empty set ; ::_thesis: for E being Subset-Family of Omega st E is intersection_stable holds
for D being Dynkin_System of Omega st E c= D holds
sigma E c= D
let E be Subset-Family of Omega; ::_thesis: ( E is intersection_stable implies for D being Dynkin_System of Omega st E c= D holds
sigma E c= D )
assume A1: E is intersection_stable ; ::_thesis: for D being Dynkin_System of Omega st E c= D holds
sigma E c= D
reconsider G = generated_Dynkin_System E as Dynkin_System of Omega ;
 G is intersection_stable by A1, Th23;
then A2: G is SigmaField of Omega by Th20;
let D be Dynkin_System of Omega; ::_thesis: ( E c= D implies sigma E c= D )
assume  E c= D ; ::_thesis: sigma E c= D
then A3: G c= D by Def6;
 E c= G by Def6;
then  sigma E c= G by A2, PROB_1:def_9;
hence  sigma E c= D by A3, XBOOLE_1:1; ::_thesis: verum
end;