let x be real number ; :: thesis: for y being real non negative number
for r, a being real positive number st a <= 1 holds
(+ x,y,r) " [.0 ,a.[ = (Ball |[x,y]|,(r * a)) /\ y>=0-plane
let y be real non negative number ; :: thesis: for r, a being real positive number st a <= 1 holds
(+ x,y,r) " [.0 ,a.[ = (Ball |[x,y]|,(r * a)) /\ y>=0-plane
let r, a be real positive number ; :: 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:66;
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 set ; :: 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:46;
then A4: (+ x,y,r) . p < a by XXREAL_1:3;
A5: p = |[(q `1 ),(q `2 )]| by EUCLID:57;
then A6: q `2 >= 0 by Lm1, Th22;
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:79;
|.(|[x,y]| - q).| = |.(q - |[x,y]|).| by TOPRNS_1:28;
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 set ; :: 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:28;
A12: p = |[(q `1 ),(q `2 )]| by EUCLID:57;
u in y>=0-plane by A8, XBOOLE_0:def 4;
then q `2 >= 0 by A12, Th22;
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:88;
then (+ x,y,r) . p < a by A10, A11, XREAL_1:66;
then (+ x,y,r) . p in [.0 ,a.[ by A13, XXREAL_1:3;
hence u in (+ x,y,r) " [.0 ,a.[ by FUNCT_2:46; :: thesis: verum