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