let X be set ; :: thesis: for D being a_partition of X holds X in UniCl D
let D be a_partition of X; :: thesis: X in UniCl D
D c= D ;
then union D in { (union P) where P is Subset of D : verum } ;
then X in { (union P) where P is Subset of D : verum } by EQREL_1:def 4;
hence X in UniCl D by Th14; :: thesis: verum