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

W = W9

let X be non empty SubSpace of XX; :: thesis: 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

let D be non empty a_partition of the carrier of X; :: thesis: 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

let W, W9 be Point of XX; :: thesis: ( not W in the carrier of X & (Proj (TrivExt D)) . W = (Proj (TrivExt D)) . W9 implies W = W9 )

assume not W in the carrier of X ; :: thesis: ( not (Proj (TrivExt D)) . W = (Proj (TrivExt D)) . W9 or W = W9 )

then A1: (Proj (TrivExt D)) . W = {W} by Th34;

W9 in (Proj (TrivExt D)) . W9 by EQREL_1:def 9;

hence ( not (Proj (TrivExt D)) . W = (Proj (TrivExt D)) . W9 or W = W9 ) by A1, TARSKI:def 1; :: thesis: verum

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

let X be non empty SubSpace of XX; :: thesis: 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

let D be non empty a_partition of the carrier of X; :: thesis: 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

let W, W9 be Point of XX; :: thesis: ( not W in the carrier of X & (Proj (TrivExt D)) . W = (Proj (TrivExt D)) . W9 implies W = W9 )

assume not W in the carrier of X ; :: thesis: ( not (Proj (TrivExt D)) . W = (Proj (TrivExt D)) . W9 or W = W9 )

then A1: (Proj (TrivExt D)) . W = {W} by Th34;

W9 in (Proj (TrivExt D)) . W9 by EQREL_1:def 9;

hence ( not (Proj (TrivExt D)) . W = (Proj (TrivExt D)) . W9 or W = W9 ) by A1, TARSKI:def 1; :: thesis: verum