let n be Nat; 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); 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); 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); ( 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}
; 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; verum