let D be Simple_closed_curve; :: thesis: for p, q being Point of (TOP-REAL 2) st p in D & q in D holds
(TOP-REAL 2) | (D \ {p}),(TOP-REAL 2) | (D \ {q}) are_homeomorphic
let p, q be Point of (TOP-REAL 2); :: thesis: ( p in D & q in D implies (TOP-REAL 2) | (D \ {p}),(TOP-REAL 2) | (D \ {q}) are_homeomorphic )
assume that
A1: p in D and
A2: q in D ; :: thesis: (TOP-REAL 2) | (D \ {p}),(TOP-REAL 2) | (D \ {q}) are_homeomorphic

per cases ( p = q or p <> q ) ;

suppose p = q ; :: thesis: (TOP-REAL 2) | (D \ {p}),(TOP-REAL 2) | (D \ {q}) are_homeomorphic

hence (TOP-REAL 2) | (D \ {p}),(TOP-REAL 2) | (D \ {q}) are_homeomorphic ; :: thesis: verum

end;

suppose p <> q ; :: thesis: (TOP-REAL 2) | (D \ {p}),(TOP-REAL 2) | (D \ {q}) are_homeomorphic

then reconsider Dp = D \ {p}, Dq = D \ {q} as non empty Subset of (TOP-REAL 2) by A1, A2, ZFMISC_1:56;
A3: (TOP-REAL 2) | Dq, I(01) are_homeomorphic by A2, Th49;
(TOP-REAL 2) | Dp, I(01) are_homeomorphic by A1, Th49;
hence (TOP-REAL 2) | (D \ {p}),(TOP-REAL 2) | (D \ {q}) are_homeomorphic by A3, BORSUK_3:3; :: thesis: verum

end;

end;