let X be non empty TopSpace; :: thesis: for D being non empty a_partition of the carrier of X
for W being Point of (space D) ex W9 being Point of X st (Proj D) . W9 = W
let D be non empty a_partition of the carrier of X; :: thesis: for W being Point of (space D) ex W9 being Point of X st (Proj D) . W9 = W
let W be Point of (space D); :: thesis: ex W9 being Point of X st (Proj D) . W9 = W
reconsider p = W as Element of D by Def7;
consider W9 being Point of X such that
A1: (proj D) . W9 = p by EQREL_1:68;
take W9 ; :: thesis: (Proj D) . W9 = W
thus (Proj D) . W9 = W by A1; :: thesis: verum