let x be Real; :: thesis: for y being non negative Real
for r, a being positive Real st a <= 1 holds
(+ (x,y,r)) " [.0,a.[ = (Ball (|[x,y]|,(r * a))) /\ y>=0-plane
let y be non negative Real; :: thesis: for r, a being positive Real st a <= 1 holds
(+ (x,y,r)) " [.0,a.[ = (Ball (|[x,y]|,(r * a))) /\ y>=0-plane
let r, a be positive Real; :: thesis: ( a <= 1 implies (+ (x,y,r)) " [.0,a.[ = (Ball (|[x,y]|,(r * a))) /\ y>=0-plane )
set f = + (x,y,r);
assume A1: a <= 1 ; :: thesis: (+ (x,y,r)) " [.0,a.[ = (Ball (|[x,y]|,(r * a))) /\ y>=0-plane
then r * a <= r * 1 by XREAL_1:64;
then A2: Ball (|[x,y]|,(r * a)) c= Ball (|[x,y]|,r) by JORDAN:18;
thus (+ (x,y,r)) " [.0,a.[ c= (Ball (|[x,y]|,(r * a))) /\ y>=0-plane :: according to XBOOLE_0:def 10 :: thesis: (Ball (|[x,y]|,(r * a))) /\ y>=0-plane c= (+ (x,y,r)) " [.0,a.[

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in (+ (x,y,r)) " [.0,a.[ or u in (Ball (|[x,y]|,(r * a))) /\ y>=0-plane )
assume A3: u in (+ (x,y,r)) " [.0,a.[ ; :: thesis: u in (Ball (|[x,y]|,(r * a))) /\ y>=0-plane
then reconsider p = u as Point of Niemytzki-plane ;
p in y>=0-plane by Lm1;
then reconsider q = p as Element of (TOP-REAL 2) ;
(+ (x,y,r)) . p in [.0,a.[ by A3, FUNCT_2:38;
then A4: (+ (x,y,r)) . p < a by XXREAL_1:3;
A5: p = |[(q `1),(q `2)]| by EUCLID:53;
then A6: q `2 >= 0 by Lm1, Th18;
then p in Ball (|[x,y]|,r) by A4, A1, A5, Def6;
then (+ (x,y,r)) . p = |.(|[x,y]| - q).| / r by A5, A6, Def6;
then A7: |.(|[x,y]| - q).| < r * a by A4, XREAL_1:77;
|.(|[x,y]| - q).| = |.(q - |[x,y]|).| by TOPRNS_1:27;
then p in Ball (|[x,y]|,(r * a)) by A7, TOPREAL9:7;
hence u in (Ball (|[x,y]|,(r * a))) /\ y>=0-plane by Lm1, XBOOLE_0:def 4; :: thesis: verum

end;

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in (Ball (|[x,y]|,(r * a))) /\ y>=0-plane or u in (+ (x,y,r)) " [.0,a.[ )
assume A8: u in (Ball (|[x,y]|,(r * a))) /\ y>=0-plane ; :: thesis: u in (+ (x,y,r)) " [.0,a.[
then reconsider p = u as Point of Niemytzki-plane by Lm1, XBOOLE_0:def 4;
reconsider q = p as Element of (TOP-REAL 2) by A8;
A9: u in Ball (|[x,y]|,(r * a)) by A8, XBOOLE_0:def 4;
then A10: |.(q - |[x,y]|).| < r * a by TOPREAL9:7;
A11: |.(|[x,y]| - q).| = |.(q - |[x,y]|).| by TOPRNS_1:27;
A12: p = |[(q `1),(q `2)]| by EUCLID:53;
u in y>=0-plane by A8, XBOOLE_0:def 4;
then q `2 >= 0 by A12, Th18;
then A13: (+ (x,y,r)) . p = |.(|[x,y]| - q).| / r by A2, A9, A12, Def6;
then r * ((+ (x,y,r)) . p) = |.(|[x,y]| - q).| by XCMPLX_1:87;
then (+ (x,y,r)) . p < a by A10, A11, XREAL_1:64;
then (+ (x,y,r)) . p in [.0,a.[ by A13, XXREAL_1:3;
hence u in (+ (x,y,r)) " [.0,a.[ by FUNCT_2:38; :: thesis: verum