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:
given r8 being Real such that A2: ( w1 = r8 * w7 or w7 = r8 * w1 ) ; :: thesis:
reconsider y1 = w1 as Element of REAL n by EUCLID:25;

per cases ;

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

then A4: a + 1 > 0 ;

now

assume A5: 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, A5, TOPRNS_1:24; :: thesis:

end;

then w1 <> 0* n by EUCLID:74;
then consider y being Element of REAL n such that
A6: 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;

A8: now

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

end;

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

A13: now

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

per cases by A14;

suppose w1 = r * w4 ; :: thesis:

then y1 = r * (((a + 1) / |.y.|) * y) by EUCLID:69;
then y1 = (r * ((a + 1) / |.y.|)) * y by A14, EUCLID:69, RVSUM_1:71;
then y1 = (r * ((a + 1) / |.y.|)) * y by RVSUM_1:71;
then y1 = (r * ((a + 1) / |.y.|)) * y' by A10, XCMPLX_0:def 7;
hence contradiction by A6; :: thesis:

end;

suppose w4 = r * w1 ; :: thesis:

then ((a + 1) / |.y.|) * y = r * y1 by EUCLID:69;
then ((((a + 1) / |.y.|) " ) * ((a + 1) / |.y.|)) * y' = (((a + 1) / |.y.|) " ) * (r * y1) by A14, RVSUM_1:71;
then ((((a + 1) / |.y.|) " ) * ((a + 1) / |.y.|)) * y = ((((a + 1) / |.y.|) " ) * r) * y1' by RVSUM_1:71;
then 1 * y = ((((a + 1) / |.y.|) " ) * r) * y1 by A10, XCMPLX_0:def 7;
then y = ((((a + 1) / |.y.|) " ) * r) * y1 by RVSUM_1:74;
hence contradiction by A6; :: thesis:

end;

then consider w2, w3 being Point of (TOP-REAL n) such that
A16: ( w2 in Q & w3 in Q & LSeg w1,w2 c= Q & LSeg w2,w3 c= Q & LSeg w3,w4 c= Q ) by A1, A12, Th49;

now

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

A18: now

assume r1 = 0 ; :: thesis:
then A19: ( w4 = 0. (TOP-REAL n) or 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, A11, A19, TOPRNS_1:24; :: thesis:

end;

per cases by A2;

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

now

per cases by A17;

case w4 = r1 * w7 ; :: thesis:

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

end;

case w7 = r1 * w4 ; :: thesis:

then (r1 " ) * w7 = ((r1 " ) * r1) * w4 by EUCLID:34;
then (r1 " ) * w7 = 1 * w4 by A18, 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 A18, XCMPLX_0:def 7;
then ((r1 " ) " ) * w4 = w7 by EUCLID:33;
then w1 = (r8 * ((r1 " ) " )) * w4 by A20, EUCLID:34;
hence contradiction by A13; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

then A22: (r8 " ) * w7 = ((r8 " ) * r8) * w1 by EUCLID:34;

now

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

end;

then (r8 " ) * w7 = 1 * w1 by A22, XCMPLX_0:def 7;
then A24: (r8 " ) * w7 = w1 by EUCLID:33;

now

per cases by A17;

case w4 = r1 * w7 ; :: thesis:

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

end;

case w7 = r1 * w4 ; :: thesis:

then (r1 " ) * w7 = ((r1 " ) * r1) * w4 by EUCLID:34;
then (r1 " ) * w7 = 1 * w4 by A18, 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 A18, XCMPLX_0:def 7;
then ((r1 " ) " ) * w4 = w7 by EUCLID:33;
then w1 = ((r8 " ) * ((r1 " ) " )) * w4 by A24, EUCLID:34;
hence contradiction by A13; :: thesis:

end;

hence contradiction ; :: thesis:

end;

then consider w2', w3' being Point of (TOP-REAL n) such that
A25: ( w2' in Q & w3' in Q & LSeg w4,w2' c= Q & LSeg w2',w3' c= Q & LSeg w3',w7 c= Q ) by A1, A12, Th49;
thus 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, A16, A25; :: thesis:

end;

suppose A26: a < 0 ; :: thesis:

A27: the carrier of (TOP-REAL n) = REAL n by EUCLID:25;
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, A26; :: thesis:

end;

then A28: Q = the carrier of (TOP-REAL n) by A27, XBOOLE_0:def 10;
set w2 = 0. (TOP-REAL n);
A29: LSeg w1,(0. (TOP-REAL n)) c= Q by A28;
LSeg (0. (TOP-REAL n)),w7 c= Q by A28;
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 A28, A29; :: thesis:

end;