set X = Niemytzki-plane ;
A1: the carrier of Niemytzki-plane = y>=0-plane by Def3;
let x, y be Point of Niemytzki-plane ; :: according to URYSOHN1:def 9 :: thesis: ( x = y or ex b₁, b₂ being Element of bool the carrier of Niemytzki-plane st
( b₁ is open & b₂ is open & x in b₁ & not y in b₁ & y in b₂ & not x in b₂ ) )
( x in y>=0-plane & y in y>=0-plane ) by A1;
then reconsider a = x, b = y as Point of (TOP-REAL 2) ;
assume x <> y ; :: thesis: ex b₁, b₂ being Element of bool the carrier of Niemytzki-plane st
( b₁ is open & b₂ is open & x in b₁ & not y in b₁ & y in b₂ & not x in b₂ )
then |.(a - b).| <> 0 by TOPRNS_1:29;
then |.(a - b).| > 0 ;
then reconsider r = |.(a - b).| as real positive number ;
consider q being Point of (TOP-REAL 2), U being open Subset of Niemytzki-plane such that
A2: ( x in U & q in U & ( for c being Point of (TOP-REAL 2) st c in U holds
|.(c - q).| < r / 2 ) ) by Th34;
consider p being Point of (TOP-REAL 2), V being open Subset of Niemytzki-plane such that
A3: ( y in V & p in V & ( for c being Point of (TOP-REAL 2) st c in V holds
|.(c - p).| < r / 2 ) ) by Th34;
take U ; :: thesis: ex b₁ being Element of bool the carrier of Niemytzki-plane st
( U is open & b₁ is open & x in U & not y in U & y in b₁ & not x in b₁ )
take V ; :: thesis: ( U is open & V is open & x in U & not y in U & y in V & not x in V )
thus ( U is open & V is open & x in U ) by A2; :: thesis: ( not y in U & y in V & not x in V )

hereby :: thesis: ( y in V & not x in V )

assume y in U ; :: thesis: contradiction
then ( |.(b - q).| < r / 2 & |.(a - q).| < r / 2 ) by A2;
then ( |.(a - b).| <= |.(a - q).| + |.(q - b).| & |.(q - b).| = |.(b - q).| & |.(a - q).| + |.(b - q).| < (r / 2) + (r / 2) ) by TOPRNS_1:28, TOPRNS_1:35, XREAL_1:10;
hence contradiction ; :: thesis: verum

end;

thus y in V by A3; :: thesis: not x in V
assume x in V ; :: thesis: contradiction
then ( |.(b - p).| < r / 2 & |.(a - p).| < r / 2 ) by A3;
then ( |.(a - b).| <= |.(a - p).| + |.(p - b).| & |.(p - b).| = |.(b - p).| & |.(a - p).| + |.(b - p).| < (r / 2) + (r / 2) ) by TOPRNS_1:28, TOPRNS_1:35, XREAL_1:10;
hence contradiction ; :: thesis: verum