theorem Th35: :: BORSUK_1:35

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
for W, W9 being Point of XX st not W in the carrier of X & (Proj (TrivExt D)) . W = (Proj (TrivExt D)) . W9 holds
W = W9