:: DYNKIN semantic presentation

begin

theorem :: DYNKIN:1
for Omega being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in rng f : ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) iff ex n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st f : ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) = x : ( ( ) ( ) set ) ) ;

theorem :: DYNKIN:2
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) is finite ;

registration
let n be ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;
cluster Segm n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) -> finite ;
end;

definition
let Omega be ( ( non empty ) ( non empty ) set ) ;
let a, b, c be ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
:: original: followed_by
redefine func (a,b) followed_by c -> ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool Omega : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non trivial ) ( non trivial ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool Omega : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non trivial ) ( non trivial ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool Omega : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non trivial ) ( non trivial ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non trivial ) ( non trivial ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;
end;

theorem :: DYNKIN:3
for a, b being ( ( ) ( ) set ) holds Union ((a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ) followed_by {} : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V18() ext-real Function-like functional finite V43() V58() ) set ) ) : ( ( ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) = a : ( ( ) ( ) set ) \/ b : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

definition
let Omega be ( ( non empty ) ( non empty ) set ) ;
let f be ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool Omega : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool Omega : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool Omega : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;
let X be ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
func seqIntersection (X,f) -> ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool Omega : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non trivial ) ( non trivial ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool Omega : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non trivial ) ( non trivial ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool Omega : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non trivial ) ( non trivial ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non trivial ) ( non trivial ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) means :: DYNKIN:def 1
 for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds it : ( ( ) ( ) set ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool Omega : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non trivial ) ( non trivial ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) = X : ( ( ) ( ) set ) /\ (f : ( ( non empty ) ( non empty ) set ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool Omega : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non trivial ) ( non trivial ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool Omega : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

begin

definition
let Omega be ( ( non empty ) ( non empty ) set ) ;
let f be ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool Omega : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool Omega : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool Omega : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;
:: original: disjoint_valued
redefine attr f is disjoint_valued means :: DYNKIN:def 2
 for n, m being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) < m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds
f : ( ( non empty ) ( non empty ) set ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool Omega : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non trivial ) ( non trivial ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) misses f : ( ( non empty ) ( non empty ) set ) . m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool Omega : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non trivial ) ( non trivial ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;
end;

theorem :: DYNKIN:4
for Y being ( ( non empty ) ( non empty ) set )
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) c= meet Y : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) iff for y being ( ( ) ( ) Element of Y : ( ( non empty ) ( non empty ) set ) ) holds x : ( ( ) ( ) set ) c= y : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) ;

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

definition
let Omega be ( ( non empty ) ( non empty ) set ) ;
let f be ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool Omega : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool Omega : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool Omega : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;
let n be ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() ) Nat) ;
func disjointify (f,n) -> ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) equals :: DYNKIN:def 3
(f : ( ( non empty ) ( non empty ) set ) . n : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool Omega : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non trivial ) ( non trivial ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) \ (union (rng (f : ( ( non empty ) ( non empty ) set ) | n : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool Omega : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

definition
let Omega be ( ( non empty ) ( non empty ) set ) ;
let g be ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool Omega : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool Omega : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool Omega : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;
func disjointify g -> ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool Omega : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non trivial ) ( non trivial ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool Omega : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non trivial ) ( non trivial ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool Omega : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non trivial ) ( non trivial ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non trivial ) ( non trivial ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) means :: DYNKIN:def 4
 for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() ) Nat) holds it : ( ( ) ( ) set ) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() ) Nat) : ( ( ) ( ) Element of bool Omega : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non trivial ) ( non trivial ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) = disjointify (g : ( ( non empty ) ( non empty ) set ) ,n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() ) Nat) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
end;

theorem :: DYNKIN:5
for Omega being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() ) Nat) holds (disjointify f : ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() ) Nat) : ( ( ) ( ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) = (f : ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() ) Nat) ) : ( ( ) ( ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) \ (union (rng (f : ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) | n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() ) Nat) ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: DYNKIN:6
for Omega being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds disjointify f : ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) is V56() ;

theorem :: DYNKIN:7
for Omega being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds union (rng (disjointify f : ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = union (rng f : ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: DYNKIN:8
for Omega being ( ( non empty ) ( non empty ) set )
for x, y being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) misses y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
(x : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) followed_by ({} Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V18() ext-real Function-like functional finite V43() V58() ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) is V56() ;

theorem :: DYNKIN:9
for Omega being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st f : ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) is V56() holds
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds seqIntersection (X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,f : ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) is V56() ;

theorem :: DYNKIN:10
for Omega being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) /\ (Union f : ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = Union (seqIntersection (X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,f : ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

begin

definition
let Omega be ( ( non empty ) ( non empty ) set ) ;
mode Dynkin_System of Omega -> ( ( ) ( ) Subset-Family of ) means :: DYNKIN:def 5
( ( for f being ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool Omega : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non trivial ) ( non trivial ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool Omega : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non trivial ) ( non trivial ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool Omega : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non trivial ) ( non trivial ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non trivial ) ( non trivial ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st rng f : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) c= it : ( ( non empty ) ( non empty ) set ) & f : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) is V56() holds
Union f : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool Omega : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( non empty ) set ) ) in it : ( ( non empty ) ( non empty ) set ) ) & ( for X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) in it : ( ( non empty ) ( non empty ) set ) holds
X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ` : ( ( ) ( ) Element of bool Omega : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( non empty ) set ) ) in it : ( ( non empty ) ( non empty ) set ) ) & {} : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V18() ext-real Function-like functional finite V43() V58() ) set ) in it : ( ( non empty ) ( non empty ) set ) );
end;

registration
let Omega be ( ( non empty ) ( non empty ) set ) ;
cluster -> non empty for ( ( ) ( ) Dynkin_System of Omega : ( ( non trivial ) ( non trivial ) set ) ) ;
end;

theorem :: DYNKIN:11
for Omega being ( ( non empty ) ( non empty ) set ) holds bool Omega : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is ( ( ) ( non empty ) Dynkin_System of Omega : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: DYNKIN:12
for F, Omega being ( ( non empty ) ( non empty ) set ) st ( for Y being ( ( ) ( ) set ) st Y : ( ( ) ( ) set ) in F : ( ( non empty ) ( non empty ) set ) holds
Y : ( ( ) ( ) set ) is ( ( ) ( non empty ) Dynkin_System of Omega : ( ( non empty ) ( non empty ) set ) ) ) holds
meet F : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) is ( ( ) ( non empty ) Dynkin_System of Omega : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: DYNKIN:13
for Omega being ( ( non empty ) ( non empty ) set )
for A, B being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for D being ( ( non empty ) ( non empty ) Subset-Family of ) st D : ( ( non empty ) ( non empty ) Subset-Family of ) is ( ( ) ( non empty ) Dynkin_System of Omega : ( ( non empty ) ( non empty ) set ) ) & D : ( ( non empty ) ( non empty ) Subset-Family of ) is intersection_stable & A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) in D : ( ( non empty ) ( non empty ) Subset-Family of ) & B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) in D : ( ( non empty ) ( non empty ) Subset-Family of ) holds
A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) \ B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) in D : ( ( non empty ) ( non empty ) Subset-Family of ) ;

theorem :: DYNKIN:14
for Omega being ( ( non empty ) ( non empty ) set )
for A, B being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for D being ( ( non empty ) ( non empty ) Subset-Family of ) st D : ( ( non empty ) ( non empty ) Subset-Family of ) is ( ( ) ( non empty ) Dynkin_System of Omega : ( ( non empty ) ( non empty ) set ) ) & D : ( ( non empty ) ( non empty ) Subset-Family of ) is intersection_stable & A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) in D : ( ( non empty ) ( non empty ) Subset-Family of ) & B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) in D : ( ( non empty ) ( non empty ) Subset-Family of ) holds
A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) \/ B : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) in D : ( ( non empty ) ( non empty ) Subset-Family of ) ;

theorem :: DYNKIN:15
for Omega being ( ( non empty ) ( non empty ) set )
for D being ( ( non empty ) ( non empty ) Subset-Family of ) st D : ( ( non empty ) ( non empty ) Subset-Family of ) is ( ( ) ( non empty ) Dynkin_System of Omega : ( ( non empty ) ( non empty ) set ) ) & D : ( ( non empty ) ( non empty ) Subset-Family of ) is intersection_stable holds
for x being ( ( finite ) ( finite ) set ) st x : ( ( finite ) ( finite ) set ) c= D : ( ( non empty ) ( non empty ) Subset-Family of ) holds
union x : ( ( finite ) ( finite ) set ) : ( ( ) ( ) set ) in D : ( ( non empty ) ( non empty ) Subset-Family of ) ;

theorem :: DYNKIN:16
for Omega being ( ( non empty ) ( non empty ) set )
for D being ( ( non empty ) ( non empty ) Subset-Family of ) st D : ( ( non empty ) ( non empty ) Subset-Family of ) is ( ( ) ( non empty ) Dynkin_System of Omega : ( ( non empty ) ( non empty ) set ) ) & D : ( ( non empty ) ( non empty ) Subset-Family of ) is intersection_stable holds
for f being ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st rng f : ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) c= D : ( ( non empty ) ( non empty ) Subset-Family of ) holds
rng (disjointify f : ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) c= D : ( ( non empty ) ( non empty ) Subset-Family of ) ;

theorem :: DYNKIN:17
for Omega being ( ( non empty ) ( non empty ) set )
for D being ( ( non empty ) ( non empty ) Subset-Family of ) st D : ( ( non empty ) ( non empty ) Subset-Family of ) is ( ( ) ( non empty ) Dynkin_System of Omega : ( ( non empty ) ( non empty ) set ) ) & D : ( ( non empty ) ( non empty ) Subset-Family of ) is intersection_stable holds
for f being ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool Omega : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) st rng f : ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) c= D : ( ( non empty ) ( non empty ) Subset-Family of ) holds
union (rng f : ( ( Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V36( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) in D : ( ( non empty ) ( non empty ) Subset-Family of ) ;

theorem :: DYNKIN:18
for Omega being ( ( non empty ) ( non empty ) set )
for D being ( ( ) ( non empty ) Dynkin_System of Omega : ( ( non empty ) ( non empty ) set ) )
for x, y being ( ( ) ( ) Element of D : ( ( ) ( non empty ) Dynkin_System of b1 : ( ( non empty ) ( non empty ) set ) ) ) st x : ( ( ) ( ) Element of b2 : ( ( ) ( non empty ) Dynkin_System of b1 : ( ( non empty ) ( non empty ) set ) ) ) misses y : ( ( ) ( ) Element of b2 : ( ( ) ( non empty ) Dynkin_System of b1 : ( ( non empty ) ( non empty ) set ) ) ) holds
x : ( ( ) ( ) Element of b2 : ( ( ) ( non empty ) Dynkin_System of b1 : ( ( non empty ) ( non empty ) set ) ) ) \/ y : ( ( ) ( ) Element of b2 : ( ( ) ( non empty ) Dynkin_System of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) in D : ( ( ) ( non empty ) Dynkin_System of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: DYNKIN:19
for Omega being ( ( non empty ) ( non empty ) set )
for D being ( ( ) ( non empty ) Dynkin_System of Omega : ( ( non empty ) ( non empty ) set ) )
for x, y being ( ( ) ( ) Element of D : ( ( ) ( non empty ) Dynkin_System of b1 : ( ( non empty ) ( non empty ) set ) ) ) st x : ( ( ) ( ) Element of b2 : ( ( ) ( non empty ) Dynkin_System of b1 : ( ( non empty ) ( non empty ) set ) ) ) c= y : ( ( ) ( ) Element of b2 : ( ( ) ( non empty ) Dynkin_System of b1 : ( ( non empty ) ( non empty ) set ) ) ) holds
y : ( ( ) ( ) Element of b2 : ( ( ) ( non empty ) Dynkin_System of b1 : ( ( non empty ) ( non empty ) set ) ) ) \ x : ( ( ) ( ) Element of b2 : ( ( ) ( non empty ) Dynkin_System of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) in D : ( ( ) ( non empty ) Dynkin_System of b1 : ( ( non empty ) ( non empty ) set ) ) ;

begin

theorem :: DYNKIN:20
for Omega being ( ( non empty ) ( non empty ) set )
for D being ( ( non empty ) ( non empty ) Subset-Family of ) st D : ( ( non empty ) ( non empty ) Subset-Family of ) is ( ( ) ( non empty ) Dynkin_System of Omega : ( ( non empty ) ( non empty ) set ) ) & D : ( ( non empty ) ( non empty ) Subset-Family of ) is intersection_stable holds
D : ( ( non empty ) ( non empty ) Subset-Family of ) is ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ;

definition
let Omega be ( ( non empty ) ( non empty ) set ) ;
let E be ( ( ) ( ) Subset-Family of ) ;
func generated_Dynkin_System E -> ( ( ) ( non empty ) Dynkin_System of Omega : ( ( non trivial ) ( non trivial ) set ) ) means :: DYNKIN:def 6
( E : ( ( non empty ) ( non empty ) set ) c= it : ( ( ) ( ) set ) & ( for D being ( ( ) ( non empty ) Dynkin_System of Omega : ( ( non trivial ) ( non trivial ) set ) ) st E : ( ( non empty ) ( non empty ) set ) c= D : ( ( ) ( non empty ) Dynkin_System of Omega : ( ( non empty ) ( non empty ) set ) ) holds
it : ( ( ) ( ) set ) c= D : ( ( ) ( non empty ) Dynkin_System of Omega : ( ( non empty ) ( non empty ) set ) ) ) );
end;

definition
let Omega be ( ( non empty ) ( non empty ) set ) ;
let G be ( ( ) ( ) set ) ;
let X be ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
func DynSys (X,G) -> ( ( ) ( ) Subset-Family of ) means :: DYNKIN:def 7
 for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
( A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) in it : ( ( ) ( ) set ) iff A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) /\ X : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool Omega : ( ( non trivial ) ( non trivial ) set ) : ( ( ) ( non empty ) set ) ) in G : ( ( non empty ) ( non empty ) set ) );
end;

definition
let Omega be ( ( non empty ) ( non empty ) set ) ;
let G be ( ( ) ( non empty ) Dynkin_System of Omega : ( ( non empty ) ( non empty ) set ) ) ;
let X be ( ( ) ( ) Element of G : ( ( ) ( non empty ) Dynkin_System of Omega : ( ( non empty ) ( non empty ) set ) ) ) ;
:: original: DynSys
redefine func DynSys (X,G) -> ( ( ) ( non empty ) Dynkin_System of Omega : ( ( non trivial ) ( non trivial ) set ) ) ;
end;

theorem :: DYNKIN:21
for Omega being ( ( non empty ) ( non empty ) set )
for E being ( ( ) ( ) Subset-Family of )
for X, Y being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) in E : ( ( ) ( ) Subset-Family of ) & Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) in generated_Dynkin_System E : ( ( ) ( ) Subset-Family of ) : ( ( ) ( non empty ) Dynkin_System of b1 : ( ( non empty ) ( non empty ) set ) ) & E : ( ( ) ( ) Subset-Family of ) is intersection_stable holds
X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) /\ Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) in generated_Dynkin_System E : ( ( ) ( ) Subset-Family of ) : ( ( ) ( non empty ) Dynkin_System of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: DYNKIN:22
for Omega being ( ( non empty ) ( non empty ) set )
for E being ( ( ) ( ) Subset-Family of )
for X, Y being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) in generated_Dynkin_System E : ( ( ) ( ) Subset-Family of ) : ( ( ) ( non empty ) Dynkin_System of b1 : ( ( non empty ) ( non empty ) set ) ) & Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) in generated_Dynkin_System E : ( ( ) ( ) Subset-Family of ) : ( ( ) ( non empty ) Dynkin_System of b1 : ( ( non empty ) ( non empty ) set ) ) & E : ( ( ) ( ) Subset-Family of ) is intersection_stable holds
X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) /\ Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) in generated_Dynkin_System E : ( ( ) ( ) Subset-Family of ) : ( ( ) ( non empty ) Dynkin_System of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: DYNKIN:23
for Omega being ( ( non empty ) ( non empty ) set )
for E being ( ( ) ( ) Subset-Family of ) st E : ( ( ) ( ) Subset-Family of ) is intersection_stable holds
generated_Dynkin_System E : ( ( ) ( ) Subset-Family of ) : ( ( ) ( non empty ) Dynkin_System of b1 : ( ( non empty ) ( non empty ) set ) ) is intersection_stable ;

theorem :: DYNKIN:24
for Omega being ( ( non empty ) ( non empty ) set )
for E being ( ( ) ( ) Subset-Family of ) st E : ( ( ) ( ) Subset-Family of ) is intersection_stable holds
for D being ( ( ) ( non empty ) Dynkin_System of Omega : ( ( non empty ) ( non empty ) set ) ) st E : ( ( ) ( ) Subset-Family of ) c= D : ( ( ) ( non empty ) Dynkin_System of b1 : ( ( non empty ) ( non empty ) set ) ) holds
sigma E : ( ( ) ( ) Subset-Family of ) : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= D : ( ( ) ( non empty ) Dynkin_System of b1 : ( ( non empty ) ( non empty ) set ) ) ;