theorem Th40: :: EQREL_1:40

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