theorem :: BORSUK_1:28

for X being non empty TopSpace
for D being non empty a_partition of the carrier of X
for W being Point of X holds W in (Proj D) . W by EQREL_1:def 9;