let Omega be non empty set ; :: thesis: bool Omega is SigmaField of Omega
set Y = bool Omega;
A1: for E being Subset of Omega st E in bool Omega holds
E ` in bool Omega ;
( bool Omega c= bool Omega & ( for BSeq being SetSequence of Omega st rng BSeq c= bool Omega holds
Intersection BSeq in bool Omega ) ) ;
hence bool Omega is SigmaField of Omega by A1, Def1, Def8; :: thesis: verum