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
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 Def7; :: thesis: verum