let n be Element of NAT ; :: thesis:
let a be Real; :: thesis:
let Q be Subset of (TOP-REAL n); :: thesis:
let w1, w7 be Point of (TOP-REAL n); :: thesis:
assume A1: ( n >= 2 & Q = { q where q is Point of (TOP-REAL n) : |.q.| > a } & w1 in Q & w7 in Q ) ; :: thesis:
reconsider y1 = w1 as Element of REAL n by EUCLID:25;
given r8 being Real such that A2: ( w1 = r8 * w7 or w7 = r8 * w1 ) ; :: thesis:

per cases ;

suppose A3: a >= 0 ; :: thesis:

now

assume A4: w1 = 0. (TOP-REAL n) ; :: thesis:
ex q being Point of (TOP-REAL n) st
( q = w1 & |.q.| > a ) by A1;
hence contradiction by A3, A4, TOPRNS_1:24; :: thesis:

end;

then w1 <> 0* n by EUCLID:74;
then consider y being Element of REAL n such that
A5: for r being Real holds
( not y = r * y1 & not y1 = r * y ) by A1, Th55;
set y4 = ((a + 1) / |.y.|) * y;
reconsider w4 = ((a + 1) / |.y.|) * y as Point of (TOP-REAL n) by EUCLID:25;

A6: now

A7: 0 * y1 = 0 * w1 by EUCLID:69
.= 0. (TOP-REAL n) by EUCLID:33
.= 0* n by EUCLID:74 ;
assume |.y.| = 0 ; :: thesis:
hence contradiction by A5, A7, EUCLID:11; :: thesis:

end;

then A8: (a + 1) / |.y.| > 0 by A3, XREAL_1:141;

A9: now

reconsider y9 = y, y19 = y1 as Element of n -tuples_on REAL ;
given r being Real such that A10: ( w1 = r * w4 or w4 = r * w1 ) ; :: thesis:

per cases by A10;

suppose w1 = r * w4 ; :: thesis:

then y1 = r * (((a + 1) / |.y.|) * y) by EUCLID:69;
then y1 = (r * ((a + 1) / |.y.|)) * y by RVSUM_1:71;
hence contradiction by A5; :: thesis:

end;

suppose w4 = r * w1 ; :: thesis:

then ((a + 1) / |.y.|) * y = r * y1 by EUCLID:69;
then ((((a + 1) / |.y.|) " ) * ((a + 1) / |.y.|)) * y9 = (((a + 1) / |.y.|) " ) * (r * y1) by RVSUM_1:71;
then ((((a + 1) / |.y.|) " ) * ((a + 1) / |.y.|)) * y = ((((a + 1) / |.y.|) " ) * r) * y19 by RVSUM_1:71;
then 1 * y = ((((a + 1) / |.y.|) " ) * r) * y1 by A8, XCMPLX_0:def 7;
then y = ((((a + 1) / |.y.|) " ) * r) * y1 by RVSUM_1:74;
hence contradiction by A5; :: thesis:

end;

A11: |.w4.| = (abs ((a + 1) / |.y.|)) * |.y.| by EUCLID:14
.= ((a + 1) / |.y.|) * |.y.| by A3, ABSVALUE:def 1
.= a + 1 by A6, XCMPLX_1:88 ;
then |.w4.| > a by XREAL_1:31;
then A12: w4 in Q by A1;

now

given r1 being Real such that A13: ( w4 = r1 * w7 or w7 = r1 * w4 ) ; :: thesis:

A14: now

assume r1 = 0 ; :: thesis:
then A15: ( w4 = 0. (TOP-REAL n) or w7 = 0. (TOP-REAL n) ) by A13, EUCLID:33;
ex q7 being Point of (TOP-REAL n) st
( q7 = w7 & |.q7.| > a ) by A1;
hence contradiction by A3, A11, A15, TOPRNS_1:24; :: thesis:

end;

per cases by A2;

suppose A16: w1 = r8 * w7 ; :: thesis:

now

per cases by A13;

case w4 = r1 * w7 ; :: thesis:

then (r1 " ) * w4 = ((r1 " ) * r1) * w7 by EUCLID:34;
then (r1 " ) * w4 = 1 * w7 by A14, XCMPLX_0:def 7;
then (r1 " ) * w4 = w7 by EUCLID:33;
then w1 = (r8 * (r1 " )) * w4 by A16, EUCLID:34;
hence contradiction by A9; :: thesis:

end;

case w7 = r1 * w4 ; :: thesis:

then (r1 " ) * w7 = ((r1 " ) * r1) * w4 by EUCLID:34;
then (r1 " ) * w7 = 1 * w4 by A14, XCMPLX_0:def 7;
then (r1 " ) * w7 = w4 by EUCLID:33;
then ((r1 " ) " ) * w4 = (((r1 " ) " ) * (r1 " )) * w7 by EUCLID:34;
then ((r1 " ) " ) * w4 = 1 * w7 by A14, XCMPLX_0:def 7;
then ((r1 " ) " ) * w4 = w7 by EUCLID:33;
then w1 = (r8 * ((r1 " ) " )) * w4 by A16, EUCLID:34;
hence contradiction by A9; :: thesis:

end;

hence contradiction ; :: thesis:

end;

suppose A17: w7 = r8 * w1 ; :: thesis:

A18: now

assume r8 = 0 ; :: thesis:
then A19: w7 = 0. (TOP-REAL n) by A17, EUCLID:33;
ex q7 being Point of (TOP-REAL n) st
( q7 = w7 & |.q7.| > a ) by A1;
hence contradiction by A3, A19, TOPRNS_1:24; :: thesis:

end;

(r8 " ) * w7 = ((r8 " ) * r8) * w1 by A17, EUCLID:34;
then (r8 " ) * w7 = 1 * w1 by A18, XCMPLX_0:def 7;
then A20: (r8 " ) * w7 = w1 by EUCLID:33;

now

per cases by A13;

case w4 = r1 * w7 ; :: thesis:

then (r1 " ) * w4 = ((r1 " ) * r1) * w7 by EUCLID:34;
then (r1 " ) * w4 = 1 * w7 by A14, XCMPLX_0:def 7;
then (r1 " ) * w4 = w7 by EUCLID:33;
then w1 = ((r8 " ) * (r1 " )) * w4 by A20, EUCLID:34;
hence contradiction by A9; :: thesis:

end;

case w7 = r1 * w4 ; :: thesis:

then (r1 " ) * w7 = ((r1 " ) * r1) * w4 by EUCLID:34;
then (r1 " ) * w7 = 1 * w4 by A14, XCMPLX_0:def 7;
then (r1 " ) * w7 = w4 by EUCLID:33;
then ((r1 " ) " ) * w4 = (((r1 " ) " ) * (r1 " )) * w7 by EUCLID:34;
then ((r1 " ) " ) * w4 = 1 * w7 by A14, XCMPLX_0:def 7;
then ((r1 " ) " ) * w4 = w7 by EUCLID:33;
then w1 = ((r8 " ) * ((r1 " ) " )) * w4 by A20, EUCLID:34;
hence contradiction by A9; :: thesis:

end;

hence contradiction ; :: thesis:

end;

then A21: ex w29, w39 being Point of (TOP-REAL n) st
( w29 in Q & w39 in Q & LSeg w4,w29 c= Q & LSeg w29,w39 c= Q & LSeg w39,w7 c= Q ) by A1, A12, Th49;
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,w4 c= Q ) by A1, A12, A9, Th49;
hence 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 A12, A21; :: thesis:

end;

suppose A22: a < 0 ; :: thesis:

set w2 = 0. (TOP-REAL n);
A23: REAL n c= Q

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in REAL n ; :: thesis:
then reconsider w = x as Point of (TOP-REAL n) by EUCLID:25;
|.w.| >= 0 ;
hence x in Q by A1, A22; :: thesis:

end;

the carrier of (TOP-REAL n) = REAL n by EUCLID:25;
then A24: Q = the carrier of (TOP-REAL n) by A23, XBOOLE_0:def 10;
then ( LSeg w1,(0. (TOP-REAL n)) c= Q & LSeg (0. (TOP-REAL n)),w7 c= Q ) ;
hence 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 A24; :: thesis:

end;