let n be Nat; :: thesis: for P being Subset of ()
for Q being Subset of (() | P)
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 (() | P)
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 (() | P); :: 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 P9 = P as non empty Subset of () by ;
consider f being Function of I,(() | P9) such that
A3: f is being_homeomorphism and
A4: f . 0 = p1 and
A5: f . 1 = p2 by ;
reconsider P7 = the carrier of I \ {0,1} as Subset of I ;
A6: f is continuous by ;
A7: f is one-to-one by ;
Q = f .: P7
proof
[#] (() | P) = P by PRE_TOPC:def 5;
then A8: rng f = P by ;
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 ;
A11: not x in {p1,p2} by ;
consider z being object such that
A12: z in dom f and
A13: x = f . z by ;
now :: thesis: not z in {0,1}
assume z in {0,1} ; :: thesis: contradiction
then ( x = p1 or x = p2 ) by ;
hence contradiction by A11, TARSKI:def 2; :: thesis: verum
end;
then z in P7 by ;
hence x in f .: P7 by ; :: 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 ;
then A18: x <> 0 by TARSKI:def 2;
A19: x <> 1 by ;
A20: y in P by ;
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, the carrier of (() | P9) ;
now :: thesis: ( ( f . x = p1 & contradiction ) or ( f . x = p2 & contradiction ) )
per cases ( f . x = p1 or f . x = p2 ) by ;
end;
end;
hence contradiction ; :: thesis: verum
end;
hence y in Q by ; :: thesis: verum
end;
hence Q is connected by ; :: thesis: verum