let x be real number ; :: thesis: for r being real positive number holds (Ball |[x,r]|,r) \/ {|[x,0 ]|} is open Subset of Niemytzki-plane
let r be real positive number ; :: thesis: (Ball |[x,r]|,r) \/ {|[x,0 ]|} is open Subset of Niemytzki-plane
A1: r is Real by XREAL_0:def 1;
the carrier of Niemytzki-plane = y>=0-plane by Def3;
then reconsider a = |[x,0 ]| as Point of Niemytzki-plane by Th22;
consider BB being Neighborhood_System of Niemytzki-plane such that
A2: 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
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;
x is Real by XREAL_0:def 1;
then BB . |[x,0 ]| = { ((Ball |[x,q]|,q) \/ {|[x,0 ]|}) where q is Element of REAL : q > 0 } by A2;
then (Ball |[x,r]|,r) \/ {|[x,0 ]|} in BB . a by A1;
hence (Ball |[x,r]|,r) \/ {|[x,0 ]|} is open Subset of Niemytzki-plane by YELLOW_8:21; :: thesis: verum