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 2
.= [:{x}, the carrier of Y:] by PRE_TOPC:8 ;
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 Th9; :: thesis: verum