let Omega be non empty set ; :: thesis: for D being a_partition of Omega holds UniCl D is Dynkin_System of Omega
let D be a_partition of Omega; :: thesis: UniCl D is Dynkin_System of Omega

now :: thesis: ( ( for f being SetSequence of Omega st rng f c= UniCl D & f is disjoint_valued holds
Union f in UniCl D ) & ( for X being Subset of Omega st X in UniCl D holds
X ` in UniCl D ) & {} in UniCl D )

hereby :: thesis: ( ( for X being Subset of Omega st X in UniCl D holds
X ` in UniCl D ) & {} in UniCl D )

let f be SetSequence of Omega; :: thesis: ( rng f c= UniCl D & f is disjoint_valued implies Union f in UniCl D )
assume that
A1: rng f c= UniCl D and
f is disjoint_valued ; :: thesis: Union f in UniCl D
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: verum

end;

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

end;

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