let X, Y be non empty TopSpace; :: thesis: for x being Point of X holds [:(X | {x}),Y:],Y are_homeomorphic
let x be Point of X; :: thesis: [:(X | {x}),Y:],Y are_homeomorphic
set Z = {x};
the carrier of [:(X | {x}),Y:] = [:the carrier of (X | {x}),the carrier of Y:] by BORSUK_1:def 5
.= [:{x},the carrier of Y:] by PRE_TOPC:29 ;
then reconsider f = pr2 {x},the carrier of Y as Function of [:(X | {x}),Y:],Y ;
take f ; :: according to T_0TOPSP:def 1 :: thesis: f is being_homeomorphism
thus f is being_homeomorphism by Th11; :: thesis: verum