let x be Real; for a, r being positive Real holds (Ball (|[x,(r * a)]|,(r * a))) \/ {|[x,0]|} c= (+ (x,r)) " [.0,a.[
let a, r be positive Real; (Ball (|[x,(r * a)]|,(r * a))) \/ {|[x,0]|} c= (+ (x,r)) " [.0,a.[
let u be object ; TARSKI:def 3 ( not u in (Ball (|[x,(r * a)]|,(r * a))) \/ {|[x,0]|} or u in (+ (x,r)) " [.0,a.[ )
assume A1:
u in (Ball (|[x,(r * a)]|,(r * a))) \/ {|[x,0]|}
; u in (+ (x,r)) " [.0,a.[
then A2:
( u in Ball (|[x,(r * a)]|,(r * a)) or u in {|[x,0]|} )
by XBOOLE_0:def 3;
reconsider p = u as Point of (TOP-REAL 2) by A1;
A3:
|[x,0]| in y>=0-plane
;
Ball (|[x,(r * a)]|,(r * a)) c= y>=0-plane
by Th20;
then reconsider q = p as Point of Niemytzki-plane by A3, A2, Lm1, TARSKI:def 1;
A4:
(+ (x,r)) . q <= 1
by BORSUK_1:40, XXREAL_1:1;
A5:
(+ (x,r)) . q >= 0
by BORSUK_1:40, XXREAL_1:1;