:: deftheorem Def9 defines proj EQREL_1:def 9 :
for X being non empty set
for D being non empty a_partition of X
for b₃ being Function of X,D holds
( b₃ = proj D iff for p being Element of X holds p in b₃ . p );