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