let Omega be non empty set ; :: thesis: bool Omega is Dynkin_System of Omega
A1: ( {} c= Omega & bool Omega c= bool Omega ) ;
( ( for f being SetSequence of Omega st rng f c= bool Omega & f is V62() 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