let p be Point of (TOP-REAL 2); :: thesis: ( p `2 >= 0 implies for x, a being real number
for r being real positive number st 0 < (+ x,r) . p & (+ x,r) . p < a & a <= 1 holds
p in Ball |[x,(r * a)]|,(r * a) )
assume A1: p `2 >= 0 ; :: thesis: for x, a being real number
for r being real positive number st 0 < (+ x,r) . p & (+ x,r) . p < a & a <= 1 holds
p in Ball |[x,(r * a)]|,(r * a)
let x, a be real number ; :: thesis: for r being real positive number st 0 < (+ x,r) . p & (+ x,r) . p < a & a <= 1 holds
p in Ball |[x,(r * a)]|,(r * a)
A2: p = |[(p `1 ),(p `2 )]| by EUCLID:57;
let r be real positive number ; :: thesis: ( 0 < (+ x,r) . p & (+ x,r) . p < a & a <= 1 implies p in Ball |[x,(r * a)]|,(r * a) )
set r1 = r * a;
assume that
A3: 0 < (+ x,r) . p and
A4: (+ x,r) . p < a and
A5: a <= 1 ; :: thesis: p in Ball |[x,(r * a)]|,(r * a)
A6: ( x <> p `1 implies p <> |[(p `1 ),0 ]| ) by A4, A5, Th65;
A7: p <> |[x,0 ]| by A3, Def5;
assume not p in Ball |[x,(r * a)]|,(r * a) ; :: thesis: contradiction
then |.(p - |[x,(r * a)]|).| >= r * a by TOPREAL9:7;
then ( |.(p - |[x,(r * a)]|).| = r * a or ( |.(p - |[x,(r * a)]|).| > r * a & ( a < 1 or a = 1 ) ) ) by A5, XXREAL_0:1;
then ( (+ x,r) . p = a or ( a < 1 & (+ x,r) . p > a ) or ( a = 1 & not p in Ball |[x,r]|,r ) ) by A1, A2, A3, A5, A7, A6, Th66, Th68, TOPREAL9:7;
hence contradiction by A1, A2, A4, A7, A6, Def5; :: thesis: verum