let n be Element of NAT ; :: thesis: for a being Real
for P being Subset of (TOP-REAL n) st n >= 2 & P = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } holds
P is connected
let a be Real; :: thesis: for P being Subset of (TOP-REAL n) st n >= 2 & P = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } holds
P is connected
let P be Subset of (TOP-REAL n); :: thesis: ( n >= 2 & P = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } implies P is connected )
assume A1: ( n >= 2 & P = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } ) ; :: thesis: P is connected
then reconsider Q = P as non empty Subset of (TOP-REAL n) by Th60, XXREAL_0:2;
for w1, w7 being Point of (TOP-REAL n) st w1 in Q & w7 in Q & w1 <> w7 holds
ex f being Function of I[01] ,((TOP-REAL n) | Q) st
( f is continuous & w1 = f . 0 & w7 = f . 1 )

proof

let w1, w7 be Point of (TOP-REAL n); :: thesis: ( w1 in Q & w7 in Q & w1 <> w7 implies ex f being Function of I[01] ,((TOP-REAL n) | Q) st
( f is continuous & w1 = f . 0 & w7 = f . 1 ) )
assume A2: ( w1 in Q & w7 in Q & w1 <> w7 ) ; :: thesis: ex f being Function of I[01] ,((TOP-REAL n) | Q) st
( f is continuous & w1 = f . 0 & w7 = f . 1 )

per cases ( for r being Real holds
( not w1 = r * w7 & not w7 = r * w1 ) or ex r being Real st
( w1 = r * w7 or w7 = r * w1 ) ) ;

suppose for r being Real holds
( not w1 = r * w7 & not w7 = r * w1 ) ; :: thesis: ex f being Function of I[01] ,((TOP-REAL n) | Q) st
( f is continuous & w1 = f . 0 & w7 = f . 1 )

then consider w2, w3 being Point of (TOP-REAL n) such that
A3: ( w2 in Q & w3 in Q & LSeg w1,w2 c= Q & LSeg w2,w3 c= Q & LSeg w3,w7 c= Q ) by A1, A2, Th50;
thus ex f being Function of I[01] ,((TOP-REAL n) | Q) st
( f is continuous & w1 = f . 0 & w7 = f . 1 ) by A2, A3, Th45; :: thesis: verum

end;

suppose ex r being Real st
( w1 = r * w7 or w7 = r * w1 ) ; :: thesis: ex f being Function of I[01] ,((TOP-REAL n) | Q) st
( f is continuous & w1 = f . 0 & w7 = f . 1 )

then consider w2, w3, w4, w5, w6 being Point of (TOP-REAL n) such that
A4: ( w2 in Q & w3 in Q & w4 in Q & w5 in Q & w6 in Q & LSeg w1,w2 c= Q & LSeg w2,w3 c= Q & LSeg w3,w4 c= Q & LSeg w4,w5 c= Q & LSeg w5,w6 c= Q & LSeg w6,w7 c= Q ) by A1, A2, Th57;
consider f1 being Function of I[01] ,((TOP-REAL n) | Q) such that
A5: ( f1 is continuous & w1 = f1 . 0 & w7 = f1 . 1 ) by A2, A4, Th46;
thus ex f being Function of I[01] ,((TOP-REAL n) | Q) st
( f is continuous & w1 = f . 0 & w7 = f . 1 ) by A5; :: thesis: verum

end;

end;

end;

hence P is connected by JORDAN1:5; :: thesis: verum