let X be set ; :: thesis: for p being a_partition of X holds {p} is Part-Family of X
let p be a_partition of X; :: thesis: {p} is Part-Family of X
{p} c= bool (bool X) by ZFMISC_1:37;
then A1: {p} is Family-Class of X ;
for x being set st x in {p} holds
x is a_partition of X by TARSKI:def 1;
hence {p} is Part-Family of X by A1, Def10; :: thesis: verum