theorem Th9: :: MYCIELSK:9

for X being set
for P being finite a_partition of X
for S being Subset of X holds
( ( for p being set st p in P holds
p meets S ) iff card (P | S) = card P )