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)
A2: p = |[(p `1 ),(p `2 )]| by EUCLID:57;
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)
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 A3: ( 0 < (+ x,r) . p & (+ x,r) . p < a & a <= 1 ) ; :: thesis: p in Ball |[x,(r * a)]|,(r * a)
then A4: ( p <> |[x,0 ]| & ( x <> p `1 implies p <> |[(p `1 ),0 ]| ) ) by Def5, Th65;
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 A3, 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, A4, Th66, Th68, TOPREAL9:7;
hence contradiction by A1, A2, A3, A4, Def5; :: thesis: verum