let n be Element of NAT ; :: thesis: for a being Real
for P being Subset of (TOP-REAL n) st P = { q where q is Point of (TOP-REAL n) : |.q.| < a } holds
P is convex
let a be Real; :: thesis: for P being Subset of (TOP-REAL n) st P = { q where q is Point of (TOP-REAL n) : |.q.| < a } holds
P is convex
let P be Subset of (TOP-REAL n); :: thesis: ( P = { q where q is Point of (TOP-REAL n) : |.q.| < a } implies P is convex )
assume A1: P = { q where q is Point of (TOP-REAL n) : |.q.| < a } ; :: thesis: P is convex
for p1, p2 being Point of (TOP-REAL n) st p1 in P & p2 in P holds
LSeg p1,p2 c= P

proof

let p1, p2 be Point of (TOP-REAL n); :: thesis: ( p1 in P & p2 in P implies LSeg p1,p2 c= P )
assume A2: ( p1 in P & p2 in P ) ; :: thesis: LSeg p1,p2 c= P
then consider q1 being Point of (TOP-REAL n) such that
A3: ( q1 = p1 & |.q1.| < a ) by A1;
consider q2 being Point of (TOP-REAL n) such that
A4: ( q2 = p2 & |.q2.| < a ) by A1, A2;
LSeg p1,p2 c= P

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in LSeg p1,p2 or x in P )
assume A5: x in LSeg p1,p2 ; :: thesis: x in P
then x in { (((1 - r) * p1) + (r * p2)) where r is Real : ( 0 <= r & r <= 1 ) } ;
then consider r being Real such that
A6: ( x = ((1 - r) * p1) + (r * p2) & 0 <= r & r <= 1 ) ;
reconsider q = x as Point of (TOP-REAL n) by A5;
A7: |.(((1 - r) * p1) + (r * p2)).| <= |.((1 - r) * p1).| + |.(r * p2).| by TOPRNS_1:30;
A8: |.((1 - r) * p1).| = (abs (1 - r)) * |.p1.| by TOPRNS_1:8;
A9: 1 - r >= 0 by A6, XREAL_1:50;
then A10: abs (1 - r) = 1 - r by ABSVALUE:def 1;

per cases ( 1 - r > 0 or 1 - r <= 0 ) ;

suppose 1 - r > 0 ; :: thesis: x in P

then A11: (abs (1 - r)) * |.p1.| < (abs (1 - r)) * a by A3, A10, XREAL_1:70;
A12: |.(r * p2).| = (abs r) * |.p2.| by TOPRNS_1:8;
0 <= abs r by COMPLEX1:132;
then A13: (abs r) * |.p2.| <= (abs r) * a by A4, XREAL_1:66;
r = abs r by A6, ABSVALUE:def 1;
then |.((1 - r) * p1).| + |.(r * p2).| < ((1 - r) * a) + (r * a) by A8, A10, A11, A12, A13, XREAL_1:10;
then |.q.| < a by A6, A7, XXREAL_0:2;
hence x in P by A1; :: thesis: verum

end;

suppose 1 - r <= 0 ; :: thesis: x in P

then A14: (1 - r) + r = 0 + r by A9;
A15: (abs (1 - r)) * |.p1.| <= (abs (1 - r)) * a by A3, A9, A10, XREAL_1:66;
A16: |.(r * p2).| = (abs r) * |.p2.| by TOPRNS_1:8;
0 < abs r by A14, ABSVALUE:def 1;
then A17: (abs r) * |.p2.| < (abs r) * a by A4, XREAL_1:70;
r = abs r by A6, ABSVALUE:def 1;
then |.((1 - r) * p1).| + |.(r * p2).| < ((1 - r) * a) + (r * a) by A8, A10, A15, A16, A17, XREAL_1:10;
then |.q.| < a by A6, A7, XXREAL_0:2;
hence x in P by A1; :: thesis: verum

end;

end;

end;

hence LSeg p1,p2 c= P ; :: thesis: verum

end;

hence P is convex by JORDAN1:def 1; :: thesis: verum