set f = + x,y,r;
consider BB being Neighborhood_System of Niemytzki-plane such that
A1: for x being Element of REAL holds BB . |[x,0 ]| = { ((Ball |[x,q]|,q) \/ {|[x,0 ]|}) where q is Element of REAL : q > 0 } and
A2: for x, y being Element of REAL st y > 0 holds
BB . |[x,y]| = { ((Ball |[x,y]|,q) /\ y>=0-plane ) where q is Element of REAL : q > 0 } by Def3;
A3: dom BB = y>=0-plane by Lm1, PARTFUN1:def 4;

now

let a, b be real number ; :: thesis: ( 0 <= a & a < 1 & 0 < b & b <= 1 implies ( (+ x,y,r) " [.0 ,b.[ is open & (+ x,y,r) " ].a,1.] is open ) )
assume that
A4: 0 <= a and
a < 1 and
A5: 0 < b and
A6: b <= 1 ; :: thesis: ( (+ x,y,r) " [.0 ,b.[ is open & (+ x,y,r) " ].a,1.] is open )
(+ x,y,r) " [.0 ,b.[ = (Ball |[x,y]|,(r * b)) /\ y>=0-plane by A5, A6, Th82;
hence (+ x,y,r) " [.0 ,b.[ is open by A5, Th32; :: thesis: (+ x,y,r) " ].a,1.] is open

now

let c be Element of Niemytzki-plane ; :: thesis: ( c in (+ x,y,r) " ].a,1.] implies ex U being Subset of Niemytzki-plane st
( b₂ in Union BB & U in b₂ & b₂ c= (+ x,y,r) " ].a,1.] ) )
c in y>=0-plane by Lm1;
then reconsider z = c as Point of (TOP-REAL 2) ;
A7: z = |[(z `1 ),(z `2 )]| by EUCLID:57;
assume c in (+ x,y,r) " ].a,1.] ; :: thesis: ex U being Subset of Niemytzki-plane st
( b₂ in Union BB & U in b₂ & b₂ c= (+ x,y,r) " ].a,1.] )
then (+ x,y,r) . c in ].a,1.] by FUNCT_1:def 13;
then A8: (+ x,y,r) . c > a by XXREAL_1:2;

per cases ( z `2 > 0 or z `2 = 0 ) by A7, Lm1, Th22;

suppose A9: z `2 > 0 ; :: thesis: ex U being Subset of Niemytzki-plane st
( b₂ in Union BB & U in b₂ & b₂ c= (+ x,y,r) " ].a,1.] )

then reconsider r1 = |.(|[x,y]| - z).| - (r * a) as real positive number by A4, A8, Th83, XREAL_1:52;
reconsider U = (Ball z,r1) /\ y>=0-plane as Subset of Niemytzki-plane by A7, A9, Th32;
U in { ((Ball |[(z `1 ),(z `2 )]|,q) /\ y>=0-plane ) where q is Element of REAL : q > 0 } by A7;
then A10: U in BB . |[(z `1 ),(z `2 )]| by A2, A9;
take U = U; :: thesis: ( U in Union BB & c in U & U c= (+ x,y,r) " ].a,1.] )
|[(z `1 ),(z `2 )]| in y>=0-plane by A9;
hence U in Union BB by A10, A3, CARD_5:10; :: thesis: ( c in U & U c= (+ x,y,r) " ].a,1.] )
c in Ball z,r1 by Th17;
hence ( c in U & U c= (+ x,y,r) " ].a,1.] ) by A4, A8, A9, Lm1, Th83, XBOOLE_0:def 4; :: thesis: verum

end;

suppose A11: z `2 = 0 ; :: thesis: ex U being Subset of Niemytzki-plane st
( b₂ in Union BB & U in b₂ & b₂ c= (+ x,y,r) " ].a,1.] )

then consider r1 being real positive number such that
r1 = (|.(|[x,y]| - z).| - (r * a)) / 2 and
A12: (Ball |[(z `1 ),r1]|,r1) \/ {z} c= (+ x,y,r) " ].a,1.] by A4, A8, Th84;
reconsider U = (Ball |[(z `1 ),r1]|,r1) \/ {z} as Subset of Niemytzki-plane by A7, A11, Th31;
r1 is Real by XREAL_0:def 1;
then U in { ((Ball |[(z `1 ),q]|,q) \/ {|[(z `1 ),0 ]|}) where q is Element of REAL : q > 0 } by A7, A11;
then A13: U in BB . |[(z `1 ),(z `2 )]| by A1, A11;
take U = U; :: thesis: ( U in Union BB & c in U & U c= (+ x,y,r) " ].a,1.] )
|[(z `1 ),(z `2 )]| in y>=0-plane by A11;
hence U in Union BB by A13, A3, CARD_5:10; :: thesis: ( c in U & U c= (+ x,y,r) " ].a,1.] )
thus c in U by SETWISEO:6; :: thesis: U c= (+ x,y,r) " ].a,1.]
thus U c= (+ x,y,r) " ].a,1.] by A12; :: thesis: verum

end;

end;

end;

hence (+ x,y,r) " ].a,1.] is open by YELLOW_9:31; :: thesis: verum

end;

hence + x,y,r is continuous by Th79; :: thesis: verum