theorem Th10: :: PUA2MSS1:11

for X being non empty set
for Y being set st Y c= X holds
for P being a_partition of X holds { (a /\ Y) where a is Element of P : a meets Y } is a_partition of Y