let n be Nat; :: thesis: for a being Real
for P being Subset of (TOP-REAL n) st n >= 2 & P = { 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 = { 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 = { q where q is Point of (TOP-REAL n) : |.q.| > a } implies P is connected )
assume A1: ( n >= 2 & P = { 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 Th37, 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 that
A2: ( w1 in Q & w7 in Q ) and
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 ex w2, w3 being Point of (TOP-REAL n) st
( w2 in Q & w3 in Q & LSeg (w1,w2) c= Q & LSeg (w2,w3) c= Q & LSeg (w3,w7) c= Q ) by A1, A2, Th29;
hence ex f being Function of I[01],((TOP-REAL n) | Q) st
( f is continuous & w1 = f . 0 & w7 = f . 1 ) by A2, Th26; :: 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 ex w2, w3, w4, w5, w6 being Point of (TOP-REAL n) st
( 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, Th35;
hence ex f being Function of I[01],((TOP-REAL n) | Q) st
( f is continuous & w1 = f . 0 & w7 = f . 1 ) by A2, Th27; :: thesis: verum

end;

end;

end;

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