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:
reconsider y1 = w1 as Element of REAL n by EUCLID:22;
assume A1: ( n >= 2 & Q = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } & w1 in Q & w7 in Q & ex r being Real st
( w1 = r * w7 or w7 = r * w1 ) ) ; :: thesis:
then consider r8 being Real such that
A2: ( w1 = r8 * w7 or w7 = r8 * w1 ) ;

per cases ;

suppose A3: a > 0 ; :: thesis:

now :: thesis:

assume w1 = 0. (TOP-REAL n) ; :: thesis:
then |.w1.| = 0 by TOPRNS_1:23;
then w1 in { q where q is Point of (TOP-REAL n) : |.q.| < a } by A3;
hence contradiction by A1, XBOOLE_0:def 5; :: thesis:

end;

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

A5: now :: thesis:

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

end;

then A7: a / |.y.| > 0 by A3, XREAL_1:139;

A8: now :: thesis:

reconsider y9 = y, y19 = y1 as Element of n -tuples_on REAL ;
given r being Real such that A9: ( w1 = r * w4 or w4 = r * w1 ) ; :: thesis:
( y1 = (r * (a / |.y.|)) * y or (((a / |.y.|) ") * (a / |.y.|)) * y9 = ((a / |.y.|) ") * (r * y1) ) by A9, RVSUM_1:49;
then ( y1 = (r * (a / |.y.|)) * y or (((a / |.y.|) ") * (a / |.y.|)) * y = (((a / |.y.|) ") * r) * y19 ) by RVSUM_1:49;
then A10: ( y1 = (r * (a / |.y.|)) * y9 or 1 * y = (((a / |.y.|) ") * r) * y1 ) by A7, XCMPLX_0:def 7;

per cases by A10, RVSUM_1:52;

suppose y1 = (r * (a / |.y.|)) * y ; :: thesis:

hence contradiction by A4; :: thesis:

end;

suppose y = (((a / |.y.|) ") * r) * y1 ; :: thesis:

hence contradiction by A4; :: thesis:

end;

A11: |.w4.| = |.(a / |.y.|).| * |.y.| by EUCLID:11
.= (a / |.y.|) * |.y.| by A3, ABSVALUE:def 1
.= a by A5, XCMPLX_1:87 ;

A12: now :: thesis:

assume w4 in { q where q is Point of (TOP-REAL n) : |.q.| < a } ; :: thesis:
then ex q being Point of (TOP-REAL n) st
( q = w4 & |.q.| < a ) ;
hence contradiction by A11; :: thesis:

end;

then A13: w4 in Q by A1, XBOOLE_0:def 5;

now :: thesis:

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

A15: now :: thesis:

assume r1 = 0 ; :: thesis:
then ( w4 = 0. (TOP-REAL n) or w7 = 0. (TOP-REAL n) ) by A14, RLVECT_1:10;
then ( |.w4.| = 0 or |.w7.| = 0 ) by TOPRNS_1:23;
then ( w4 in { q where q is Point of (TOP-REAL n) : |.q.| < a } or w7 in { q2 where q2 is Point of (TOP-REAL n) : |.q2.| < a } ) by A3;
hence contradiction by A1, A12, XBOOLE_0:def 5; :: thesis:

end;

now :: thesis:

per cases by A2;

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

now :: thesis:

per cases by A14;

case w4 = r1 * w7 ; :: thesis:

then (r1 ") * w4 = ((r1 ") * r1) * w7 by RLVECT_1:def 7;
then (r1 ") * w4 = 1 * w7 by A15, 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 A8; :: thesis:

end;

case w7 = r1 * w4 ; :: thesis:

then (r1 ") * w7 = ((r1 ") * r1) * w4 by RLVECT_1:def 7;
then (r1 ") * w7 = 1 * w4 by A15, 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 A15, 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 A8; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

A18: now :: thesis:

assume r8 = 0 ; :: thesis:
then w7 = 0. (TOP-REAL n) by A17, RLVECT_1:10;
then |.w7.| = 0 by TOPRNS_1:23;
then w7 in { q where q is Point of (TOP-REAL n) : |.q.| < a } by A3;
hence contradiction by A1, XBOOLE_0:def 5; :: 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 A19: (r8 ") * w7 = w1 by RLVECT_1:def 8;

now :: thesis:

per cases by A14;

case w4 = r1 * w7 ; :: thesis:

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

end;

case w7 = r1 * w4 ; :: thesis:

then (r1 ") * w7 = ((r1 ") * r1) * w4 by RLVECT_1:def 7;
then (r1 ") * w7 = 1 * w4 by A15, 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 A15, XCMPLX_0:def 7;
then ((r1 ") ") * w4 = w7 by RLVECT_1:def 8;
then w1 = ((r8 ") * ((r1 ") ")) * w4 by A19, RLVECT_1:def 7;
hence contradiction by A8; :: thesis:

end;

hence contradiction ; :: thesis:

end;

hence contradiction ; :: thesis:

end;

then A20: 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, A13, Th30;
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, A13, A8, Th30;
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 A13, A20; :: thesis:

end;

suppose A21: a <= 0 ; :: thesis:

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:

A23: now :: thesis:

assume x in { q where q is Point of (TOP-REAL n) : |.q.| < a } ; :: thesis:
then ex q being Point of (TOP-REAL n) st
( q = x & |.q.| < a ) ;
hence contradiction by A21; :: thesis:

end;

assume x in REAL n ; :: thesis:
hence x in Q by A1, A23, XBOOLE_0:def 5; :: thesis:

end;

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