let D be Simple_closed_curve; :: thesis: for p being Point of (TOP-REAL 2) st p in D holds
(TOP-REAL 2) | (D \ {p}), I(01) are_homeomorphic
let p be Point of (TOP-REAL 2); :: thesis: ( p in D implies (TOP-REAL 2) | (D \ {p}), I(01) are_homeomorphic )
assume A1: p in D ; :: thesis: (TOP-REAL 2) | (D \ {p}), I(01) are_homeomorphic
consider q being Point of (TOP-REAL 2) such that
A2: ( q in D & p <> q ) by Th4;
consider P1, P2 being non empty Subset of (TOP-REAL 2) such that
A3: P1 is_an_arc_of p,q and
A4: P2 is_an_arc_of p,q and
A5: D = P1 \/ P2 and
A6: P1 /\ P2 = {p,q} by A1, A2, TOPREAL2:5;
not q in {p} by A2, TARSKI:def 1;
then reconsider R2p = D \ {p} as non empty Subset of (TOP-REAL 2) by A2, XBOOLE_0:def 5;
A7: D \ {p} = (P1 \ {p}) \/ (P2 \ {p}) by A5, XBOOLE_1:42;
P2 is_an_arc_of q,p by A4, JORDAN5B:14;
then (TOP-REAL 2) | R2p, I(01) are_homeomorphic by A2, A3, A6, A7, Th76;
hence (TOP-REAL 2) | (D \ {p}), I(01) are_homeomorphic ; :: thesis: verum