let n be 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:22;
given r8 being Real such that A2: ( w1 = r8 * w7 or w7 = r8 * w1 ) ; :: thesis:

per cases ;

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

now :: thesis:

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:23; :: thesis:

end;

then w1 <> 0* n by EUCLID:70;
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, Th34;
set y4 = ((a + 1) / |.y.|) * y;
reconsider w4 = ((a + 1) / |.y.|) * y as Point of (TOP-REAL n) by EUCLID:22;

A6: now :: thesis:

A7: 0 * y1 = 0 * w1
.= 0. (TOP-REAL n) by RLVECT_1:10
.= 0* n by EUCLID:70 ;
assume |.y.| = 0 ; :: thesis:
hence contradiction by A5, A7, EUCLID:8; :: thesis:

end;

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

A9: now :: thesis:

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 RVSUM_1:49;
hence contradiction by A5; :: thesis:

end;

suppose w4 = r * w1 ; :: thesis:

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

end;

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

now :: thesis:

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

A14: now :: thesis:

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

end;

per cases by A2;

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

now :: thesis:

per cases by A13;

case w4 = r1 * w7 ; :: thesis:

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

end;

case w7 = r1 * w4 ; :: thesis:

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

end;

hence contradiction ; :: thesis:

end;

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

A18: now :: thesis:

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

end;

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

now :: thesis:

per cases by A13;

case w4 = r1 * w7 ; :: thesis:

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

end;

case w7 = r1 * w4 ; :: thesis:

then (r1 ") * w7 = ((r1 ") * r1) * w4 by RLVECT_1:def 7;
then (r1 ") * w7 = 1 * w4 by A14, XCMPLX_0:def 7;
then (r1 ") * w7 = w4 by RLVECT_1:def 8;
then ((r1 ") ") * w4 = (((r1 ") ") * (r1 ")) * w7 by RLVECT_1:def 7;
then ((r1 ") ") * w4 = 1 * w7 by A14, XCMPLX_0:def 7;
then ((r1 ") ") * w4 = w7 by RLVECT_1:def 8;
then w1 = ((r8 ") * ((r1 ") ")) * w4 by A20, RLVECT_1:def 7;
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, Th29;
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, Th29;
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 object ; :: according to TARSKI:def 3 :: thesis:
assume x in REAL n ; :: thesis:
then reconsider w = x as Point of (TOP-REAL n) by EUCLID:22;
|.w.| >= 0 ;
hence x in Q by A1, A22; :: thesis:

end;

the carrier of (TOP-REAL n) = REAL n by EUCLID:22;
then A24: Q = the carrier of (TOP-REAL n) by A23;
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;