let Omega, F be non empty set ; :: thesis: ( ( for Y being set st Y in F holds
Y is Dynkin_System of Omega ) implies meet F is Dynkin_System of Omega )
assume A1: for Y being set st Y in F holds
Y is Dynkin_System of Omega ; :: thesis: meet F is Dynkin_System of Omega

now :: thesis: for Y being set st Y in F holds
{} in Y

let Y be set ; :: thesis: ( Y in F implies {} in Y )
assume Y in F ; :: thesis: {} in Y
then Y is Dynkin_System of Omega by A1;
hence {} in Y by Def5; :: thesis: verum

end;

then A2: {} in meet F by SETFAM_1:def 1;

A3: now :: thesis: for f being SetSequence of Omega st rng f c= meet F & f is disjoint_valued holds
Union f in meet F

let f be SetSequence of Omega; :: thesis: ( rng f c= meet F & f is disjoint_valued implies Union f in meet F )
assume that
A4: rng f c= meet F and
A5: f is disjoint_valued ; :: thesis: Union f in meet F

now :: thesis: for Y being set st Y in F holds
Union f in Y

let Y be set ; :: thesis: ( Y in F implies Union f in Y )
assume A6: Y in F ; :: thesis: Union f in Y
meet F c= Y by A6, SETFAM_1:3;
then A7: rng f c= Y by A4;
Y is Dynkin_System of Omega by A1, A6;
hence Union f in Y by A5, A7, Def5; :: thesis: verum

end;

hence Union f in meet F by SETFAM_1:def 1; :: thesis: verum

end;

A8: now :: thesis: for X being Subset of Omega st X in meet F holds
X ` in meet F

let X be Subset of Omega; :: thesis: ( X in meet F implies X ` in meet F )
assume A9: X in meet F ; :: thesis: X ` in meet F
for Y being set st Y in F holds
X ` in Y

proof

let Y be set ; :: thesis: ( Y in F implies X ` in Y )
assume Y in F ; :: thesis: X ` in Y
then ( Y is Dynkin_System of Omega & meet F c= Y ) by A1, SETFAM_1:3;
hence X ` in Y by A9, Def5; :: thesis: verum

end;

hence X ` in meet F by SETFAM_1:def 1; :: thesis: verum

end;

set Y = the Element of F;
A10: meet F c= the Element of F by SETFAM_1:3;
the Element of F is Dynkin_System of Omega by A1;
then meet F is Subset-Family of Omega by A10, XBOOLE_1:1;
hence meet F is Dynkin_System of Omega by A3, A8, A2, Def5; :: thesis: verum