theorem Th80: :: TOPGEN_5:80

for p being Point of (TOP-REAL 2) st p `2 = 0 holds
for x being Real
for a being non negative Real
for y, r being positive Real st (+ (x,y,r)) . p > a holds
( |.(|[x,y]| - p).| > r * a & ex r1 being positive Real st
( r1 = (|.(|[x,y]| - p).| - (r * a)) / 2 & (Ball (|[(p `1),r1]|,r1)) \/ {p} c= (+ (x,y,r)) " ].a,1.] ) )