theorem :: EQREL_1:66

for X being non empty set
for D being non empty a_partition of X
for p being Element of D holds p = (proj D) " {p}