let F, Omega 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

A2: now

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

now

let Y be set ; :: thesis: ( Y in F implies Union f in Y )
assume A4: Y in F ; :: thesis: Union f in Y
A5: Y is Dynkin_System of Omega by A1, A4;
meet F c= Y by A4, SETFAM_1:4;
then rng f c= Y by A3, XBOOLE_1:1;
hence Union f in Y by A3, A5, Def7; :: thesis: verum

end;

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

end;

A6: now

let X be Subset of Omega; :: thesis: ( X in meet F implies X ` in meet F )
assume A7: 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 A8: Y in F ; :: thesis: X ` in Y
A9: Y is Dynkin_System of Omega by A1, A8;
meet F c= Y by A8, SETFAM_1:4;
hence X ` in Y by A7, A9, Def7; :: thesis: verum

end;

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

end;

consider Y being Element of F;
A10: Y is Dynkin_System of Omega by A1;
meet F c= Y by SETFAM_1:4;
then A11: meet F is Subset-Family of Omega by A10, XBOOLE_1:1;

now

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

end;

then {} in meet F by SETFAM_1:def 1;
hence meet F is Dynkin_System of Omega by A2, A6, A11, Def7; :: thesis: verum