let X, Y be non empty TopSpace; :: thesis: for x being Point of X
for Z being non empty Subset of X st Z = {x} holds
[:Y,(X | Z):],Y are_homeomorphic
let x be Point of X; :: thesis: for Z being non empty Subset of X st Z = {x} holds
[:Y,(X | Z):],Y are_homeomorphic
let Z be non empty Subset of X; :: thesis: ( Z = {x} implies [:Y,(X | Z):],Y are_homeomorphic )
assume Z = {x} ; :: thesis: [:Y,(X | Z):],Y are_homeomorphic
then A1: [:(X | Z),Y:],Y are_homeomorphic by Th15;
A2: [:Y,(X | Z):],[:(X | Z),Y:] are_homeomorphic by YELLOW12:44;
consider f being Function of [:(X | Z),Y:],Y such that
A3: f is being_homeomorphism by A1, T_0TOPSP:def 1;
consider g being Function of [:Y,(X | Z):],[:(X | Z),Y:] such that
A4: g is being_homeomorphism by A2, T_0TOPSP:def 1;
reconsider gf = f * g as Function of [:Y,(X | Z):],Y ;
gf is being_homeomorphism by A3, A4, TOPS_2:71;
hence [:Y,(X | Z):],Y are_homeomorphic by T_0TOPSP:def 1; :: thesis: verum