let n be Nat; :: thesis: for P, P1, P2 being Subset of ()
for Q being Subset of (() | P)
for p1, p2 being Point of () 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 (); :: thesis: for Q being Subset of (() | P)
for p1, p2 being Point of () 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 (() | P); :: thesis: for p1, p2 being Point of () 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 (); :: 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 () ;
A5: P21 is compact by ;
p1 in P1 /\ P2 by ;
then A6: p1 in P2 by XBOOLE_0:def 4;
A7: [#] (() | P) = P by PRE_TOPC:def 5;
then reconsider P29 = P21 as Subset of (() | P) by ;
p2 in P1 /\ P2 by ;
then A8: p2 in P2 by XBOOLE_0:def 4;
P29 is compact by ;
then A9: P29 is closed by COMPTS_1:7;
A10: P \ P2 = (P1 \ P2) \/ (P2 \ P2) by
.= (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 ;
then not x in {p1,p2} by ;
hence x in Q by ; :: 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 ;
not x in {p1,p2} by ;
then not x in P2 by ;
hence x in P1 \ P2 by ; :: thesis: verum
end;
then P1 \ P2 = Q by A11;
then Q = P29 ` by ;
hence Q is open by ; :: thesis: verum