let n be Element of NAT ; :: thesis:
let P, P1, P2 be Subset of (TOP-REAL n); :: thesis:
let Q be Subset of ((TOP-REAL n) | P); :: thesis:
let p1, p2 be Point of (TOP-REAL n); :: thesis:
assume A1: ( p1 in P & p2 in P & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1 /\ P2 = {p1,p2} & Q = P1 \ {p1,p2} ) ; :: thesis:
reconsider P21 = P2 as Subset of (TOP-REAL n) ;
A2: P21 is compact by A1, JORDAN5A:1;
p1 in P1 /\ P2 by A1, TARSKI:def 2;
then A3: ( p1 in P1 & p1 in P2 ) by XBOOLE_0:def 4;
A4: [#] ((TOP-REAL n) | P) = P by PRE_TOPC:def 10;
reconsider P2' = P21 as Subset of ((TOP-REAL n) | P) by A1, A4, XBOOLE_1:7;
p2 in P1 /\ P2 by A1, TARSKI:def 2;
then A6: ( p2 in P1 & p2 in P2 ) by XBOOLE_0:def 4;
P2' is compact by A2, A4, COMPTS_1:11;
then A8: P2' is closed by COMPTS_1:16;
A9: P \ P2 = (P1 \ P2) \/ (P2 \ P2) by A1, XBOOLE_1:42
.= (P1 \ P2) \/ {} by XBOOLE_1:37
.= P1 \ P2 ;
P1 \ P2 = Q

A10: P1 \ P2 c= Q

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in P1 \ P2 ; :: thesis:
then A11: ( x in P1 & not x in P2 ) by XBOOLE_0:def 5;
then not x in {p1,p2} by A3, A6, TARSKI:def 2;
hence x in Q by A1, A11, XBOOLE_0:def 5; :: thesis:

end;

Q c= P1 \ P2

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in Q ; :: thesis:
then A12: ( x in P1 & not x in {p1,p2} ) by A1, XBOOLE_0:def 5;
then not x in P2 by A1, XBOOLE_0:def 4;
hence x in P1 \ P2 by A12, XBOOLE_0:def 5; :: thesis:

end;

hence P1 \ P2 = Q by A10, XBOOLE_0:def 10; :: thesis:

end;

then Q = P2' ` by A4, A9, SUBSET_1:def 5;
hence Q is open by A8, TOPS_1:29; :: thesis: