:: deftheorem defines TrivExt BORSUK_1:def 9 :
for XX being non empty TopSpace
for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X holds TrivExt D = D \/ { {p} where p is Point of XX : not p in the carrier of X } ;