let n be Element of NAT ; :: thesis:
let P 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: ( P is_an_arc_of p1,p2 & Q = P \ {p1,p2} ) ; :: thesis:
then reconsider P' = P as non empty Subset of (TOP-REAL n) by TOPREAL1:4;
consider f being Function of I[01] ,((TOP-REAL n) | P') such that
A2: ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) by A1, TOPREAL1:def 2;
reconsider f1 = f as Function ;
A3: f " is being_homeomorphism by A2, TOPS_2:70;
reconsider g = f " as Function of ((TOP-REAL n) | P),I[01] ;
reconsider g1 = g as Function ;
reconsider R = the carrier of I[01] \ {0 ,1} as Subset of I[01] ;
A4: [#] I[01] <> {} ;
A5: R is open by Th41;
A6: f is one-to-one by A2, TOPS_2:def 5;
A7: g is one-to-one by A3, TOPS_2:def 5;
A8: g is continuous by A2, TOPS_2:def 5;
A9: [#] I[01] = dom f by A2, TOPS_2:def 5;
0 in [#] I[01] by BORSUK_1:83, XXREAL_1:1;
then A10: 0 in dom f by A2, TOPS_2:def 5;
1 in [#] I[01] by BORSUK_1:83, XXREAL_1:1;
then A11: 1 in dom f by A2, TOPS_2:def 5;
rng f = [#] ((TOP-REAL n) | P) by A2, TOPS_2:def 5;
then A12: (f " ) " = f by A6, TOPS_2:64;
rng g = [#] I[01] by A3, TOPS_2:def 5;
then A13: g1 " = f1 by A7, A12, TOPS_2:def 4;
g " R = (g1 " the carrier of I[01] ) \ (g1 " {0 ,1}) by FUNCT_1:138
.= ((g1 " ) .: the carrier of I[01] ) \ (g1 " {0 ,1}) by A7, FUNCT_1:155
.= (f1 .: ([#] I[01] )) \ (f1 .: {0 ,1}) by A7, A13, FUNCT_1:155
.= (rng f) \ (f .: {0 ,1}) by A9, RELAT_1:146
.= ([#] ((TOP-REAL n) | P)) \ (f .: {0 ,1}) by A2, TOPS_2:def 5
.= P \ (f .: {0 ,1}) by PRE_TOPC:def 10
.= Q by A1, A2, A10, A11, FUNCT_1:118 ;
hence Q is open by A4, A5, A8, TOPS_2:55; :: thesis: