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 = (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 ) ;
reconsider y1 = w1 as Element of REAL n by EUCLID:25;

per cases ;

suppose A3: a > 0 ; :: thesis:

now

assume w1 = 0. (TOP-REAL n) ; :: thesis:
then |.w1.| = 0 by TOPRNS_1:24;
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:74;
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, Th55;
set y4 = (a / |.y.|) * y;
reconsider w4 = (a / |.y.|) * y as Point of (TOP-REAL n) by EUCLID:25;

A6: now

assume |.y.| = 0 ; :: thesis:
then A7: 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 A4, A7; :: thesis:

end;

then A8: a / |.y.| > 0 by A3, XREAL_1:141;
A9: |.w4.| = (abs (a / |.y.|)) * |.y.| by EUCLID:14
.= (a / |.y.|) * |.y.| by A8, ABSVALUE:def 1
.= a by A6, XCMPLX_1:88 ;

A10: now

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

end;

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

A12: now

given r being Real such that A13: ( w1 = r * w4 or w4 = r * w1 ) ; :: thesis:
reconsider y' = y, y1' = y1 as Element of n -tuples_on REAL ;
( y1 = r * ((a / |.y.|) * y) or (a / |.y.|) * y = r * y1 ) by A13, EUCLID:69;
then ( y1 = (r * (a / |.y.|)) * y or (((a / |.y.|) " ) * (a / |.y.|)) * y' = ((a / |.y.|) " ) * (r * y1) ) by A13, RVSUM_1:71;
then ( y1 = (r * (a / |.y.|)) * y or (((a / |.y.|) " ) * (a / |.y.|)) * y = (((a / |.y.|) " ) * r) * y1' ) by RVSUM_1:71;
then A14: ( y1 = (r * (a / |.y.|)) * y' or 1 * y = (((a / |.y.|) " ) * r) * y1 ) by A8, XCMPLX_0:def 7;

per cases by A14, RVSUM_1:74;

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;

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

now

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

A17: now

assume r1 = 0 ; :: thesis:
then ( w4 = 0. (TOP-REAL n) or w7 = 0. (TOP-REAL n) ) by A16, EUCLID:33;
then ( |.w4.| = 0 or |.w7.| = 0 ) by TOPRNS_1:24;
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, A10, XBOOLE_0:def 5; :: thesis:

end;

now

per cases by A2;

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

now

per cases by A16;

case w4 = r1 * w7 ; :: thesis:

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

end;

case w7 = r1 * w4 ; :: thesis:

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

end;

hence contradiction ; :: thesis:

end;

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

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

now

assume r8 = 0 ; :: thesis:
then w7 = 0. (TOP-REAL n) by A19, EUCLID:33;
then |.w7.| = 0 by TOPRNS_1:24;
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;

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

now

per cases by A16;

case w4 = r1 * w7 ; :: thesis:

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

end;

case w7 = r1 * w4 ; :: thesis:

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

end;

hence contradiction ; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

end;

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

A24: 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 A25: x in REAL n ; :: thesis:

now

assume x in { q where q is Point of (TOP-REAL n) : |.q.| < a } ; :: thesis:
then consider q being Point of (TOP-REAL n) such that
A26: ( q = x & |.q.| < a ) ;
thus contradiction by A23, A26; :: thesis:

end;

hence x in Q by A1, A25, XBOOLE_0:def 5; :: thesis:

end;

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

end;