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 connected
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 connected
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 connected
let p1, p2 be Point of (TOP-REAL n); :: thesis: ( P is_an_arc_of p1,p2 & Q = P \ {p1,p2} implies Q is connected )
assume that
A1: P is_an_arc_of p1,p2 and
A2: Q = P \ {p1,p2} ; :: thesis: Q is connected
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 P7 = the carrier of I[01] \ {0,1} as Subset of I[01] ;
A6: f is continuous by A3, TOPS_2:def 5;
A7: f is one-to-one by A3, TOPS_2:def 5;
Q = f .: P7

proof

[#] ((TOP-REAL n) | P) = P by PRE_TOPC:def 5;
then A8: rng f = P by A3, TOPS_2:def 5;
thus Q c= f .: P7 :: according to XBOOLE_0:def 10 :: thesis: f .: P7 c= Q

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Q or x in f .: P7 )
assume A9: x in Q ; :: thesis: x in f .: P7
then A10: x in P by A2, XBOOLE_0:def 5;
A11: not x in {p1,p2} by A2, A9, XBOOLE_0:def 5;
consider z being object such that
A12: z in dom f and
A13: x = f . z by A8, A10, FUNCT_1:def 3;

now :: thesis: not z in {0,1}

assume z in {0,1} ; :: thesis: contradiction
then ( x = p1 or x = p2 ) by A4, A5, A13, TARSKI:def 2;
hence contradiction by A11, TARSKI:def 2; :: thesis: verum

end;

then z in P7 by A12, XBOOLE_0:def 5;
hence x in f .: P7 by A12, A13, FUNCT_1:def 6; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: P7 or y in Q )
assume y in f .: P7 ; :: thesis: y in Q
then consider x being object such that
A14: x in dom f and
A15: x in P7 and
A16: y = f . x by FUNCT_1:def 6;
A17: not x in {0,1} by A15, XBOOLE_0:def 5;
then A18: x <> 0 by TARSKI:def 2;
A19: x <> 1 by A17, TARSKI:def 2;
A20: y in P by A8, A14, A16, FUNCT_1:def 3;

now :: thesis: not y in {p1,p2}

assume A21: y in {p1,p2} ; :: thesis: contradiction
reconsider f1 = f as Function of the carrier of I[01], the carrier of ((TOP-REAL n) | P9) ;

now :: thesis: ( ( f . x = p1 & contradiction ) or ( f . x = p2 & contradiction ) )

per cases ( f . x = p1 or f . x = p2 ) by A16, A21, TARSKI:def 2;

case A22: f . x = p1 ; :: thesis: contradiction

dom f1 = the carrier of I[01] by FUNCT_2:def 1;
then 0 in dom f1 by BORSUK_1:40, XXREAL_1:1;
hence contradiction by A4, A7, A14, A18, A22, FUNCT_1:def 4; :: thesis: verum

end;

case A23: f . x = p2 ; :: thesis: contradiction

dom f1 = the carrier of I[01] by FUNCT_2:def 1;
then 1 in dom f1 by BORSUK_1:40, XXREAL_1:1;
hence contradiction by A5, A7, A14, A19, A23, FUNCT_1:def 4; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence y in Q by A2, A20, XBOOLE_0:def 5; :: thesis: verum

end;

hence Q is connected by A6, Th36, TOPS_2:61; :: thesis: verum