let n be Nat; :: thesis: for P 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 P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds

Q is open

let P 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 P is_an_arc_of p1,p2 & Q = P \ {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 P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds

Q is open

let p1, p2 be Point of (TOP-REAL n); :: 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 (TOP-REAL n) by A1, TOPREAL1:1;

consider f being Function of I[01],((TOP-REAL n) | P9) such that

A3: f is being_homeomorphism and

A4: f . 0 = p1 and

A5: f . 1 = p2 by A1, TOPREAL1:def 1;

reconsider f1 = f as Function ;

A6: f " is being_homeomorphism by A3, TOPS_2:56;

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] ;

A7: [#] I[01] <> {} ;

A8: R is open by Th34;

A9: f is one-to-one by A3, TOPS_2:def 5;

A10: g is one-to-one by A6, TOPS_2:def 5;

A11: g is continuous by A3, TOPS_2:def 5;

A12: [#] I[01] = dom f by A3, TOPS_2:def 5;

0 in [#] I[01] by BORSUK_1:40, XXREAL_1:1;

then A13: 0 in dom f by A3, TOPS_2:def 5;

1 in [#] I[01] by BORSUK_1:40, XXREAL_1:1;

then A14: 1 in dom f by A3, TOPS_2:def 5;

rng f = [#] ((TOP-REAL n) | P) by A3, TOPS_2:def 5;

then A15: (f ") " = f by A9, TOPS_2:51;

rng g = [#] I[01] by A6, TOPS_2:def 5;

then g is onto by FUNCT_2:def 3;

then A16: g1 " = f1 by A10, A15, TOPS_2:def 4;

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 A10, FUNCT_1:85

.= (f1 .: ([#] I[01])) \ (f1 .: {0,1}) by A10, A16, FUNCT_1:85

.= (rng f) \ (f .: {0,1}) by A12, RELAT_1:113

.= ([#] ((TOP-REAL n) | P)) \ (f .: {0,1}) by A3, TOPS_2:def 5

.= P \ (f .: {0,1}) by PRE_TOPC:def 5

.= Q by A2, A4, A5, A13, A14, FUNCT_1:60 ;

hence Q is open by A7, A8, A11, TOPS_2:43; :: thesis: verum

for Q being Subset of ((TOP-REAL n) | P)

for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds

Q is open

let P 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 P is_an_arc_of p1,p2 & Q = P \ {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 P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds

Q is open

let p1, p2 be Point of (TOP-REAL n); :: 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 (TOP-REAL n) by A1, TOPREAL1:1;

consider f being Function of I[01],((TOP-REAL n) | P9) such that

A3: f is being_homeomorphism and

A4: f . 0 = p1 and

A5: f . 1 = p2 by A1, TOPREAL1:def 1;

reconsider f1 = f as Function ;

A6: f " is being_homeomorphism by A3, TOPS_2:56;

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] ;

A7: [#] I[01] <> {} ;

A8: R is open by Th34;

A9: f is one-to-one by A3, TOPS_2:def 5;

A10: g is one-to-one by A6, TOPS_2:def 5;

A11: g is continuous by A3, TOPS_2:def 5;

A12: [#] I[01] = dom f by A3, TOPS_2:def 5;

0 in [#] I[01] by BORSUK_1:40, XXREAL_1:1;

then A13: 0 in dom f by A3, TOPS_2:def 5;

1 in [#] I[01] by BORSUK_1:40, XXREAL_1:1;

then A14: 1 in dom f by A3, TOPS_2:def 5;

rng f = [#] ((TOP-REAL n) | P) by A3, TOPS_2:def 5;

then A15: (f ") " = f by A9, TOPS_2:51;

rng g = [#] I[01] by A6, TOPS_2:def 5;

then g is onto by FUNCT_2:def 3;

then A16: g1 " = f1 by A10, A15, TOPS_2:def 4;

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 A10, FUNCT_1:85

.= (f1 .: ([#] I[01])) \ (f1 .: {0,1}) by A10, A16, FUNCT_1:85

.= (rng f) \ (f .: {0,1}) by A12, RELAT_1:113

.= ([#] ((TOP-REAL n) | P)) \ (f .: {0,1}) by A3, TOPS_2:def 5

.= P \ (f .: {0,1}) by PRE_TOPC:def 5

.= Q by A2, A4, A5, A13, A14, FUNCT_1:60 ;

hence Q is open by A7, A8, A11, TOPS_2:43; :: thesis: verum