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

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

hence
Q is connected
by A6, Th36, TOPS_2:61; :: thesis: verum
[#] ((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

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;

end;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 y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: P7 or y in Q )
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;

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

end;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}

then
z in P7
by A12, XBOOLE_0:def 5;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 ( x = p1 or x = p2 ) by A4, A5, A13, TARSKI:def 2;

hence contradiction by A11, TARSKI:def 2; :: thesis: verum

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

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}

hence
y in Q
by A2, A20, XBOOLE_0:def 5; :: thesis: verumassume 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) ;

end;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 ) )end;

hence
contradiction
; :: thesis: verumper cases
( f . x = p1 or f . x = p2 )
by A16, A21, TARSKI:def 2;

end;

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;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

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;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