:: deftheorem defines Proj BORSUK_1:def 8 :
for X being non empty TopSpace
for D being non empty a_partition of the carrier of X holds Proj D = proj D;