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
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 A2: 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) ;
A3: p = |[(q `1 ),(q `2 )]| by EUCLID:57;
(+ x,y,r) . p in [.0 ,a.[ by A2, FUNCT_2:46;
then A4: (+ x,y,r) . p < a by XXREAL_1:3;
then A5: ( (+ x,y,r) . p < 1 & q `2 >= 0 ) by A1, A3, Lm1, Th22, XXREAL_0:2;
then p in Ball |[x,y]|,r by A3, Def6;
then (+ x,y,r) . p = |.(|[x,y]| - q).| / r by A3, A5, Def6;
then ( |.(|[x,y]| - q).| = |.(q - |[x,y]|).| & |.(|[x,y]| - q).| < r * a ) by A4, TOPRNS_1:28, XREAL_1:79;
then p in Ball |[x,y]|,(r * a) by 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 A6: u in (Ball |[x,y]|,(r * a)) /\ y>=0-plane ; :: thesis: u in (+ x,y,r) " [.0 ,a.[
then A7: ( u in Ball |[x,y]|,(r * a) & u in y>=0-plane ) by XBOOLE_0:def 4;
reconsider p = u as Point of Niemytzki-plane by A6, Lm1, XBOOLE_0:def 4;
reconsider q = p as Element of (TOP-REAL 2) by A6;
A8: p = |[(q `1 ),(q `2 )]| by EUCLID:57;
then A9: q `2 >= 0 by A7, Th22;
r * a <= r * 1 by A1, XREAL_1:66;
then Ball |[x,y]|,(r * a) c= Ball |[x,y]|,r by JORDAN:18;
then (+ x,y,r) . p = |.(|[x,y]| - q).| / r by A7, A8, A9, Def6;
then ( (+ x,y,r) . p in [.0 ,1.] & r * ((+ x,y,r) . p) = |.(|[x,y]| - q).| & |.(q - |[x,y]|).| < r * a & |.(|[x,y]| - q).| = |.(q - |[x,y]|).| ) by A7, BORSUK_1:83, FUNCT_2:7, TOPREAL9:7, TOPRNS_1:28, XCMPLX_1:88;
then ( (+ x,y,r) . p >= 0 & (+ x,y,r) . p < a ) by XREAL_1:66;
then (+ x,y,r) . p in [.0 ,a.[ by XXREAL_1:3;
hence u in (+ x,y,r) " [.0 ,a.[ by FUNCT_2:46; :: thesis: verum