set X = Niemytzki-plane ;
consider B being Neighborhood_System of Niemytzki-plane such that
A1: for x being Element of REAL holds B . |[x,0 ]| = { ((Ball |[x,r]|,r) \/ {|[x,0 ]|}) where r is Element of REAL : r > 0 } and
A2: for x, y being Element of REAL st y > 0 holds
B . |[x,y]| = { ((Ball |[x,y]|,r) /\ y>=0-plane ) where r is Element of 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

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} )
uB is open by YELLOW_9:28;
then 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 2;
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:57;

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

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 Element of 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 number 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, Th80;
take f = f; :: thesis: ( f . x = 0 & f .: (V ` ) c= {1} )
thus f . x = 0 by A9, A12, EUCLID:57; :: thesis: f .: (V ` ) c= {1}
thus f .: (V ` ) c= {1} :: thesis: verum

proof

let u be set ; :: 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:116;
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:31;
b = |[(c `1 ),(c `2 )]| by EUCLID:57;
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 Element of 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 number 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, Th85;
take f = f; :: thesis: ( f . x = 0 & f .: (V ` ) c= {1} )
thus f . x = 0 by A20, EUCLID:57; :: thesis: f .: (V ` ) c= {1}
thus f .: (V ` ) c= {1} :: thesis: verum

proof

let u be set ; :: 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:116;
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:31;
b = |[(c `1 ),(c `2 )]| by EUCLID:57;
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 Th56, Th86; :: thesis: verum