let XX be non empty TopSpace; :: thesis: for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for W being Point of XX st not W in the carrier of X holds
(Proj (TrivExt D)) . W = {W}
let X be non empty SubSpace of XX; :: thesis: for D being non empty a_partition of the carrier of X
for W being Point of XX st not W in the carrier of X holds
(Proj (TrivExt D)) . W = {W}
let D be non empty a_partition of the carrier of X; :: thesis: for W being Point of XX st not W in the carrier of X holds
(Proj (TrivExt D)) . W = {W}
let W be Point of XX; :: thesis: ( not W in the carrier of X implies (Proj (TrivExt D)) . W = {W} )
assume not W in the carrier of X ; :: thesis: (Proj (TrivExt D)) . W = {W}
then ( W in {W} & {W} in TrivExt D ) by Th32, TARSKI:def 1;
hence (Proj (TrivExt D)) . W = {W} by EQREL_1:65; :: thesis: verum