let n be Nat; :: thesis: for P being Subset of ()
for Q being Subset of (() | P)
for p1, p2 being Point of () st P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds
Q is open

let P be Subset of (); :: thesis: for Q being Subset of (() | P)
for p1, p2 being Point of () st P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds
Q is open

let Q be Subset of (() | P); :: thesis: for p1, p2 being Point of () st P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds
Q is open

let p1, p2 be Point of (); :: thesis: ( P is_an_arc_of p1,p2 & Q = P \ {p1,p2} implies Q is open )
assume that
A1: P is_an_arc_of p1,p2 and
A2: Q = P \ {p1,p2} ; :: thesis: Q is open
reconsider P9 = P as non empty Subset of () by ;
consider f being Function of I[01],(() | P9) such that
A3: f is being_homeomorphism and
A4: f . 0 = p1 and
A5: f . 1 = p2 by ;
reconsider f1 = f as Function ;
A6: f " is being_homeomorphism by ;
reconsider g = f " as Function of (() | P),I[01] ;
reconsider g1 = g as Function ;
reconsider R = the carrier of I[01] \ {0,1} as Subset of I[01] ;
A7: [#] I[01] <> {} ;
A8: R is open by Th34;
A9: f is one-to-one by ;
A10: g is one-to-one by ;
A11: g is continuous by ;
A12: [#] I[01] = dom f by ;
0 in [#] I[01] by ;
then A13: 0 in dom f by ;
1 in [#] I[01] by ;
then A14: 1 in dom f by ;
rng f = [#] (() | P) by ;
then A15: (f ") " = f by ;
rng g = [#] I[01] by ;
then g is onto by FUNCT_2:def 3;
then A16: g1 " = f1 by ;
g " R = (g1 " the carrier of I[01]) \ (g1 " {0,1}) by FUNCT_1:69
.= ((g1 ") .: the carrier of I[01]) \ (g1 " {0,1}) by
.= (f1 .: ()) \ (f1 .: {0,1}) by
.= (rng f) \ (f .: {0,1}) by
.= ([#] (() | P)) \ (f .: {0,1}) by
.= P \ (f .: {0,1}) by PRE_TOPC:def 5
.= Q by ;
hence Q is open by ; :: thesis: verum