let n be Element of NAT ; :: thesis: for P being Subset of
for Q being Subset of
for p1, p2 being Point of st P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds
Q is connected
let P be Subset of ; :: thesis: for Q being Subset of
for p1, p2 being Point of st P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds
Q is connected
let Q be Subset of ; :: thesis: for p1, p2 being Point of st P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds
Q is connected
let p1, p2 be Point of ; :: 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 P' = P as non empty Subset of by A1, TOPREAL1:4;
consider f being Function of I[01] ,((TOP-REAL n) | P') such that
A3: f is being_homeomorphism and
A4: f . 0 = p1 and
A5: f . 1 = p2 by A1, TOPREAL1:def 2;
reconsider P7 = the carrier of I[01] \ {0 ,1} as Subset of ;
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 10;
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 set ; :: 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 set such that
A12: z in dom f and
A13: x = f . z by A8, A10, FUNCT_1:def 5;

now

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 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
A14: x in dom f and
A15: x in P7 and
A16: y = f . x by FUNCT_1:def 12;
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 5;

now

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) | P') ;

now

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:83, XXREAL_1:1;
hence contradiction by A4, A7, A14, A18, A22, FUNCT_1:def 8; :: 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:83, XXREAL_1:1;
hence contradiction by A5, A7, A14, A19, A23, FUNCT_1:def 8; :: 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, Th48, TOPS_2:75; :: thesis: verum