set X = Niemytzki-plane ;
A1: the carrier of Niemytzki-plane = y>=0-plane by Def3;
consider B being Neighborhood_System of Niemytzki-plane such that
A2: 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
A3: 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;

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 A4: ( x in V & 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 A4, TOPS_2:def 1;
then consider V' being Subset of Niemytzki-plane such that
A5: ( V' in B . x & V' c= V ) by A4, YELLOW_8:def 2;
x in y>=0-plane by A1;
then reconsider x' = x as Point of (TOP-REAL 2) ;
A6: x = |[(x' `1 ),(x' `2 )]| by EUCLID:57;

per cases ( x' `2 = 0 or x' `2 > 0 ) by A1, A6, Th22;

suppose A7: x' `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 |[(x' `1 ),r]|,r) \/ {|[(x' `1 ),0 ]|}) where r is Element of REAL : r > 0 } by A2, A6;
then consider r being Real such that
A8: ( V' = (Ball |[(x' `1 ),r]|,r) \/ {|[(x' `1 ),0 ]|} & r > 0 ) by A5;
consider f being continuous Function of Niemytzki-plane ,I[01] such that
A9: ( f . |[(x' `1 ),0 ]| = 0 & ( for a, b being real number holds
( ( |[a,b]| in V' ` implies f . |[a,b]| = 1 ) & ( |[a,b]| in V' \ {|[(x' `1 ),0 ]|} implies f . |[a,b]| = (|.(|[(x' `1 ),0 ]| - |[a,b]|).| ^2 ) / ((2 * r) * b) ) ) ) ) by A8, Th80;
take f = f; :: thesis: ( f . x = 0 & f .: (V ` ) c= {1} )
thus f . x = 0 by A7, A9, 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
A10: ( b in V ` & u = f . b ) by FUNCT_2:116;
b in y>=0-plane by A1;
then reconsider c = b as Element of (TOP-REAL 2) ;
V ` c= V' ` by A5, SUBSET_1:31;
then ( b in V' ` & b = |[(c `1 ),(c `2 )]| ) by A10, EUCLID:57;
then u = 1 by A9, A10;
hence u in {1} by TARSKI:def 1; :: thesis: verum

end;

end;

suppose A11: x' `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 |[(x' `1 ),(x' `2 )]|,r) /\ y>=0-plane ) where r is Element of REAL : r > 0 } by A3, A6;
then consider r being Real such that
A12: ( V' = (Ball |[(x' `1 ),(x' `2 )]|,r) /\ y>=0-plane & r > 0 ) by A5;
consider f being continuous Function of Niemytzki-plane ,I[01] such that
A13: ( f . |[(x' `1 ),(x' `2 )]| = 0 & ( for a, b being real number holds
( ( |[a,b]| in V' ` implies f . |[a,b]| = 1 ) & ( |[a,b]| in V' implies f . |[a,b]| = |.(|[(x' `1 ),(x' `2 )]| - |[a,b]|).| / r ) ) ) ) by A11, A12, Th85;
take f = f; :: thesis: ( f . x = 0 & f .: (V ` ) c= {1} )
thus f . x = 0 by A13, 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 ` & u = f . b ) by FUNCT_2:116;
b in y>=0-plane by A1;
then reconsider c = b as Element of (TOP-REAL 2) ;
V ` c= V' ` by A5, SUBSET_1:31;
then ( b in V' ` & b = |[(c `1 ),(c `2 )]| ) by A14, EUCLID:57;
then u = 1 by A13, A14;
hence u in {1} by TARSKI:def 1; :: thesis: verum

end;

end;

end;

end;

hence Niemytzki-plane is Tychonoff by Th56, Th86; :: thesis: verum