let n be Nat; :: thesis: for P, P1, P2 being Subset of (TOP-REAL n)
for Q being Subset of ((TOP-REAL n) | P)
for p1, p2 being Point of (TOP-REAL n) st P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1 /\ P2 = {p1,p2} & Q = P1 \ {p1,p2} holds
Q is open
let P, P1, P2 be Subset of (TOP-REAL n); :: thesis: for Q being Subset of ((TOP-REAL n) | P)
for p1, p2 being Point of (TOP-REAL n) st P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1 /\ P2 = {p1,p2} & Q = P1 \ {p1,p2} holds
Q is open
let Q be Subset of ((TOP-REAL n) | P); :: thesis: for p1, p2 being Point of (TOP-REAL n) st P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1 /\ P2 = {p1,p2} & Q = P1 \ {p1,p2} holds
Q is open
let p1, p2 be Point of (TOP-REAL n); :: thesis: ( P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1 /\ P2 = {p1,p2} & Q = P1 \ {p1,p2} implies Q is open )
assume that
A1: P2 is_an_arc_of p1,p2 and
A2: P1 \/ P2 = P and
A3: P1 /\ P2 = {p1,p2} and
A4: Q = P1 \ {p1,p2} ; :: thesis: Q is open
reconsider P21 = P2 as Subset of (TOP-REAL n) ;
A5: P21 is compact by A1, JORDAN5A:1;
p1 in P1 /\ P2 by A3, TARSKI:def 2;
then A6: p1 in P2 by XBOOLE_0:def 4;
A7: [#] ((TOP-REAL n) | P) = P by PRE_TOPC:def 5;
then reconsider P29 = P21 as Subset of ((TOP-REAL n) | P) by A2, XBOOLE_1:7;
p2 in P1 /\ P2 by A3, TARSKI:def 2;
then A8: p2 in P2 by XBOOLE_0:def 4;
P29 is compact by A5, A7, COMPTS_1:2;
then A9: P29 is closed by COMPTS_1:7;
A10: P \ P2 = (P1 \ P2) \/ (P2 \ P2) by A2, XBOOLE_1:42
.= (P1 \ P2) \/ {} by XBOOLE_1:37
.= P1 \ P2 ;
A11: P1 \ P2 c= Q

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P1 \ P2 or x in Q )
assume A12: x in P1 \ P2 ; :: thesis: x in Q
then A13: x in P1 by XBOOLE_0:def 5;
not x in P2 by A12, XBOOLE_0:def 5;
then not x in {p1,p2} by A6, A8, TARSKI:def 2;
hence x in Q by A4, A13, XBOOLE_0:def 5; :: thesis: verum

end;

Q c= P1 \ P2

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Q or x in P1 \ P2 )
assume A14: x in Q ; :: thesis: x in P1 \ P2
then A15: x in P1 by A4, XBOOLE_0:def 5;
not x in {p1,p2} by A4, A14, XBOOLE_0:def 5;
then not x in P2 by A3, A15, XBOOLE_0:def 4;
hence x in P1 \ P2 by A15, XBOOLE_0:def 5; :: thesis: verum

end;

then P1 \ P2 = Q by A11;
then Q = P29 ` by A7, A10, SUBSET_1:def 4;
hence Q is open by A9, TOPS_1:3; :: thesis: verum