let Omega be non empty set ; :: thesis: bool Omega is Dynkin_System of Omega
A1: ( ( for f being SetSequence of Omega st rng f c= bool Omega & f is disjoint_valued holds
Union f in bool Omega ) & ( for X being Subset of Omega st X in bool Omega holds
X ` in bool Omega ) ) ;
{} c= Omega by XBOOLE_1:2;
then ( bool Omega c= bool Omega & {} in bool Omega ) ;
hence bool Omega is Dynkin_System of Omega by A1, Def7; :: thesis: verum