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

proof

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Q or x in f .: P7 )
assume x in Q ; :: thesis: x in f .: P7
then A6: ( x in P & not x in {p1,p2} ) by A1, XBOOLE_0:def 5;
then consider z being set such that
A7: ( z in dom f & x = f . z ) by A5, FUNCT_1:def 5;

now

assume z in {0 ,1} ; :: thesis: contradiction
then ( x = p1 or x = p2 ) by A2, A7, TARSKI:def 2;
hence contradiction by A6, TARSKI:def 2; :: thesis: verum

end;

then z in P7 by A7, XBOOLE_0:def 5;
hence x in f .: P7 by A7, FUNCT_1:def 12; :: thesis: verum

end;

let y be set ; :: 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 set such that
A8: ( x in dom f & x in P7 & y = f . x ) by FUNCT_1:def 12;
( x in the carrier of I[01] & not x in {0 ,1} ) by A8, XBOOLE_0:def 5;
then A9: ( x <> 0 & x <> 1 ) by TARSKI:def 2;
A10: y in P by A5, A8, FUNCT_1:def 5;

now

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

now

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

case A12: 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:83, XXREAL_1:1;
hence contradiction by A2, A4, A8, A9, A12, FUNCT_1:def 8; :: thesis: verum

end;

case A13: 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:83, XXREAL_1:1;
hence contradiction by A2, A4, A8, A9, A13, FUNCT_1:def 8; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence y in Q by A1, A10, XBOOLE_0:def 5; :: thesis: verum

end;

hence Q is connected by A3, A4, TOPS_2:75; :: thesis: verum