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

now :: thesis:

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

end;

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

A3: now :: thesis:

let f be SetSequence of Omega; :: thesis:
assume that
A4: rng f c= meet F and
A5: f is V62() ; :: thesis:

now :: thesis:

let Y be set ; :: thesis:
assume A6: Y in F ; :: thesis:
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:

end;

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

end;

A8: now :: thesis:

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

proof

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

end;

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

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: