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 e being set st e in the carrier of X holds
(Proj (TrivExt D)) . e in the carrier of (space D)