defpred S₁[ 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) & S₁[x] ) ) from XFAMILY:sch 1();
bool Omega is Dynkin_System of Omega by Th10;
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 Th11;
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 Th3; :: 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