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, W' being Point of XX st not W in the carrier of X & (Proj (TrivExt D)) . W = (Proj (TrivExt D)) . W' holds
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, W' being Point of XX st not W in the carrier of X & (Proj (TrivExt D)) . W = (Proj (TrivExt D)) . W' holds
W = W'
let D be non empty a_partition of the carrier of X; :: thesis: for W, W' being Point of XX st not W in the carrier of X & (Proj (TrivExt D)) . W = (Proj (TrivExt D)) . W' holds
W = W'
let W, W' be Point of XX; :: thesis: ( not W in the carrier of X & (Proj (TrivExt D)) . W = (Proj (TrivExt D)) . W' implies W = W' )
assume not W in the carrier of X ; :: thesis: ( not (Proj (TrivExt D)) . W = (Proj (TrivExt D)) . W' or W = W' )
then A1: (Proj (TrivExt D)) . W = {W} by Th77;
W' in (Proj (TrivExt D)) . W' by Def1;
hence ( not (Proj (TrivExt D)) . W = (Proj (TrivExt D)) . W' or W = W' ) by A1, TARSKI:def 1; :: thesis: verum