let x be Real; for r being positive Real holds (Ball (|[x,r]|,r)) \/ {|[x,0]|} is open Subset of Niemytzki-plane
let r be positive Real; (Ball (|[x,r]|,r)) \/ {|[x,0]|} is open Subset of Niemytzki-plane
the carrier of Niemytzki-plane = y>=0-plane
by Def3;
then reconsider a = |[x,0]| as Point of Niemytzki-plane by Th18;
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
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;
BB . |[x,0]| = { ((Ball (|[x,q]|,q)) \/ {|[x,0]|}) where q is Real : q > 0 }
by A1;
then
(Ball (|[x,r]|,r)) \/ {|[x,0]|} in BB . a
;
hence
(Ball (|[x,r]|,r)) \/ {|[x,0]|} is open Subset of Niemytzki-plane
by YELLOW_8:12; verum