let Omega be non empty set ; :: thesis:
let D be a_partition of Omega; :: thesis:

hereby :: thesis:

let f be SetSequence of Omega; :: thesis:
assume that
A1: rng f c= UniCl D and
f is V344() ; :: thesis:
UniCl D c= bool Omega ;
then rng f c= bool Omega by A1;
then reconsider a = rng f as Subset-Family of Omega ;
union a in UniCl D by A1, ROUGHS_4:def 3;
hence Union f in UniCl D by CARD_3:def 4; :: thesis:

end;

thus for X being Subset of Omega st X in UniCl D holds
X ` in UniCl D by PROB_1:def 1; :: thesis:
UniCl D is with_empty_element ;
hence {} in UniCl D ; :: thesis:

end;

hence UniCl D is Dynkin_System of Omega by DYNKIN:def 5; :: thesis: