for X being non empty set
for p1, p2 being Element of X
for P being a_partition of X
for A being Element of P st p1 in A & (proj P) . p1 = (proj P) . p2 holds
p2 in A