set X = Niemytzki-plane ;
consider B being Neighborhood_System of Niemytzki-plane such that
A1: for x being Real holds B . |[x,0]| = { ((Ball (|[x,r]|,r)) \/ {|[x,0]|}) where r is Real : r > 0 } and
A2: for x, y being Real st y > 0 holds
B . |[x,y]| = { ((Ball (|[x,y]|,r)) /\ y>=0-plane) where r is Real : r > 0 } by Def3;
reconsider uB = Union B as prebasis of Niemytzki-plane by YELLOW_9:27;
A3: the carrier of Niemytzki-plane = y>=0-plane by Def3;

now :: thesis: for x being Point of Niemytzki-plane
for V being Subset of Niemytzki-plane st x in V & V in uB holds
ex f being continuous Function of Niemytzki-plane,I[01] st
( f . x = 0 & f .: (V `) c= {1} )

let x be Point of Niemytzki-plane; :: thesis: for V being Subset of Niemytzki-plane st x in V & V in uB holds
ex f being continuous Function of Niemytzki-plane,I[01] st
( b₄ . f = 0 & b₄ .: (b₃ `) c= {1} )
let V be Subset of Niemytzki-plane; :: thesis: ( x in V & V in uB implies ex f being continuous Function of Niemytzki-plane,I[01] st
( b<sub>3</sub> . f = 0 & b<sub>3</sub> .: (b<sub>2</sub> `) c= {1} ) )
assume that
A4: x in V and
A5: V in uB ; :: thesis: ex f being continuous Function of Niemytzki-plane,I[01] st
( b₃ . f = 0 & b₃ .: (b₂ `) c= {1} )
V is open by A5, TOPS_2:def 1;
then consider V9 being Subset of Niemytzki-plane such that
A6: V9 in B . x and
A7: V9 c= V by A4, YELLOW_8:def 1;
x in y>=0-plane by A3;
then reconsider x9 = x as Point of (TOP-REAL 2) ;
A8: x = |[(x9 `1),(x9 `2)]| by EUCLID:53;

per cases ( x9 `2 = 0 or x9 `2 > 0 ) by A3, A8, Th18;

suppose A9: x9 `2 = 0 ; :: thesis: ex f being continuous Function of Niemytzki-plane,I[01] st
( b<sub>3</sub> . f = 0 & b<sub>3</sub> .: (b<sub>2</sub> `) c= {1} )

then B . x = { ((Ball (|[(x9 `1),r]|,r)) \/ {|[(x9 `1),0]|}) where r is Real : r > 0 } by A1, A8;
then consider r being Real such that
A10: V9 = (Ball (|[(x9 `1),r]|,r)) \/ {|[(x9 `1),0]|} and
A11: r > 0 by A6;
consider f being continuous Function of Niemytzki-plane,I[01] such that
A12: f . |[(x9 `1),0]| = 0 and
A13: for a, b being Real holds
( ( |[a,b]| in V9 ` implies f . |[a,b]| = 1 ) & ( |[a,b]| in V9 \ {|[(x9 `1),0]|} implies f . |[a,b]| = (|.(|[(x9 `1),0]| - |[a,b]|).| ^2) / ((2 * r) * b) ) ) by A10, A11, Th76;
take f = f; :: thesis: ( f . x = 0 & f .: (V `) c= {1} )
thus f . x = 0 by A9, A12, EUCLID:53; :: thesis: f .: (V `) c= {1}
thus f .: (V `) c= {1} :: thesis: verum

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in f .: (V `) or u in {1} )
assume u in f .: (V `) ; :: thesis: u in {1}
then consider b being Point of Niemytzki-plane such that
A14: b in V ` and
A15: u = f . b by FUNCT_2:65;
b in y>=0-plane by A3;
then reconsider c = b as Element of (TOP-REAL 2) ;
A16: V ` c= V9 ` by A7, SUBSET_1:12;
b = |[(c `1),(c `2)]| by EUCLID:53;
then u = 1 by A16, A14, A13, A15;
hence u in {1} by TARSKI:def 1; :: thesis: verum

end;

end;

suppose A17: x9 `2 > 0 ; :: thesis: ex f being continuous Function of Niemytzki-plane,I[01] st
( b<sub>3</sub> . f = 0 & b<sub>3</sub> .: (b<sub>2</sub> `) c= {1} )

then B . x = { ((Ball (|[(x9 `1),(x9 `2)]|,r)) /\ y>=0-plane) where r is Real : r > 0 } by A2, A8;
then consider r being Real such that
A18: V9 = (Ball (|[(x9 `1),(x9 `2)]|,r)) /\ y>=0-plane and
A19: r > 0 by A6;
consider f being continuous Function of Niemytzki-plane,I[01] such that
A20: f . |[(x9 `1),(x9 `2)]| = 0 and
A21: for a, b being Real holds
( ( |[a,b]| in V9 ` implies f . |[a,b]| = 1 ) & ( |[a,b]| in V9 implies f . |[a,b]| = |.(|[(x9 `1),(x9 `2)]| - |[a,b]|).| / r ) ) by A17, A18, A19, Th81;
take f = f; :: thesis: ( f . x = 0 & f .: (V `) c= {1} )
thus f . x = 0 by A20, EUCLID:53; :: thesis: f .: (V `) c= {1}
thus f .: (V `) c= {1} :: thesis: verum

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in f .: (V `) or u in {1} )
assume u in f .: (V `) ; :: thesis: u in {1}
then consider b being Point of Niemytzki-plane such that
A22: b in V ` and
A23: u = f . b by FUNCT_2:65;
b in y>=0-plane by A3;
then reconsider c = b as Element of (TOP-REAL 2) ;
A24: V ` c= V9 ` by A7, SUBSET_1:12;
b = |[(c `1),(c `2)]| by EUCLID:53;
then u = 1 by A24, A22, A21, A23;
hence u in {1} by TARSKI:def 1; :: thesis: verum

end;

end;

end;

end;

hence Niemytzki-plane is Tychonoff by Th52, Th82; :: thesis: verum