set T = Niemytzki-plane ;
let p, q be Point of Niemytzki-plane ; :: according to URYSOHN1:def 9 :: thesis: ( p = q or ex b₁, b₂ being Element of bool the carrier of Niemytzki-plane st
( b₁ is open & b₂ is open & p in b₁ & not q in b₁ & q in b₂ & not p in b₂ ) )
assume A1: p <> q ; :: thesis: ex b₁, b₂ being Element of bool the carrier of Niemytzki-plane st
( b₁ is open & b₂ is open & p in b₁ & not q in b₁ & q in b₂ & not p in b₂ )
( p in the carrier of Niemytzki-plane & q in the carrier of Niemytzki-plane & the carrier of Niemytzki-plane = y>=0-plane ) by Def3;
then reconsider p' = p, q' = q as Point of (TOP-REAL 2) ;
p' - q' <> 0. (TOP-REAL 2) by A1, EUCLID:47;
then ( |.(p' - q').| <> 0 & |.(p' - q').| >= 0 ) by EUCLID_2:64;
then reconsider r = |.(p' - q').| as positive Real ;
consider ap being Point of (TOP-REAL 2), Up being open Subset of Niemytzki-plane such that
A2: ( p in Up & ap in Up & ( for b being Point of (TOP-REAL 2) st b in Up holds
|.(b - ap).| < r / 2 ) ) by Th34;
consider aq being Point of (TOP-REAL 2), Uq being open Subset of Niemytzki-plane such that
A3: ( q in Uq & aq in Uq & ( for b being Point of (TOP-REAL 2) st b in Uq holds
|.(b - aq).| < r / 2 ) ) by Th34;
take Up ; :: thesis: ex b₁ being Element of bool the carrier of Niemytzki-plane st
( Up is open & b₁ is open & p in Up & not q in Up & q in b₁ & not p in b₁ )
take Uq ; :: thesis: ( Up is open & Uq is open & p in Up & not q in Up & q in Uq & not p in Uq )
thus ( Up is open & Uq is open & p in Up ) by A2; :: thesis: ( not q in Up & q in Uq & not p in Uq )
thus not q in Up :: thesis: ( q in Uq & not p in Uq )

proof

assume q in Up ; :: thesis: contradiction
then ( |.(q' - ap).| = |.(ap - q').| & |.(q' - ap).| < r / 2 & |.(p' - ap).| < r / 2 ) by A2, TOPRNS_1:28;
then ( |.(p' - ap).| + |.(ap - q').| < (r / 2) + (r / 2) & |.(p' - ap).| + |.(ap - q').| >= r ) by TOPRNS_1:35, XREAL_1:10;
hence contradiction ; :: thesis: verum

end;

thus q in Uq by A3; :: thesis: not p in Uq
assume p in Uq ; :: thesis: contradiction
then ( |.(q' - aq).| = |.(aq - q').| & |.(q' - aq).| < r / 2 & |.(p' - aq).| < r / 2 ) by A3, TOPRNS_1:28;
then ( |.(p' - aq).| + |.(aq - q').| < (r / 2) + (r / 2) & |.(p' - aq).| + |.(aq - q').| >= r ) by TOPRNS_1:35, XREAL_1:10;
hence contradiction ; :: thesis: verum