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

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