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

now

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 Def7; :: thesis: verum

end;

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

A3: now

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

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:4;
then A7: rng f c= Y by A4, XBOOLE_1:1;
Y is Dynkin_System of Omega by A1, A6;
hence Union f in Y by A5, A7, Def7; :: thesis: verum

end;

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

end;

A8: now

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:4;
hence X ` in Y by 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: meet F c= Y by SETFAM_1:4;
Y 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, Def7; :: thesis: verum