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

now :: thesis: for a, b being Real st 0 <= a & a < 1 & 0 < b & b <= 1 holds
( (+ (x,y,r)) " [.0,b.[ is open & (+ (x,y,r)) " ].a,1.] is open )

let a, b be Real; :: 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, Th78;
hence (+ (x,y,r)) " [.0,b.[ is open by A5, Th28; :: thesis: (+ (x,y,r)) " ].a,1.] is open

now :: thesis: for c being Element of Niemytzki-plane st c in (+ (x,y,r)) " ].a,1.] holds
ex U being Subset of Niemytzki-plane st
( U in Union BB & c in U & U c= (+ (x,y,r)) " ].a,1.] )

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:53;
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 7;
then A8: (+ (x,y,r)) . c > a by XXREAL_1:2;

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

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 positive Real by A4, A8, Th79, XREAL_1:50;
reconsider U = (Ball (z,r1)) /\ y>=0-plane as Subset of Niemytzki-plane by A7, A9, Th28;
U in { ((Ball (|[(z `1),(z `2)]|,q)) /\ y>=0-plane) where q is 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:2; :: thesis: ( c in U & U c= (+ (x,y,r)) " ].a,1.] )
c in Ball (z,r1) by Th13;
hence ( c in U & U c= (+ (x,y,r)) " ].a,1.] ) by A4, A8, A9, Lm1, Th79, 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 positive Real 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, Th80;
reconsider U = (Ball (|[(z `1),r1]|,r1)) \/ {z} as Subset of Niemytzki-plane by A7, A11, Th27;
U in { ((Ball (|[(z `1),q]|,q)) \/ {|[(z `1),0]|}) where q is 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:2; :: thesis: ( c in U & U c= (+ (x,y,r)) " ].a,1.] )
thus c in U by ZFMISC_1:136; :: 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 Th75; :: thesis: verum