for X being set
for p being a_partition of X holds {p} is Part-Family of X