for X being non empty set
for PX being a_partition of X
for Pi being set st Pi in PX holds
ex x being Element of X st x in Pi