set T = Niemytzki-plane ;
let p, q be Point of ; :: 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₂ )
A2: q in the carrier of Niemytzki-plane ;
A3: the carrier of Niemytzki-plane = y>=0-plane by Def3;
p in the carrier of Niemytzki-plane ;
then reconsider p' = p, q' = q as Point of by A2, A3;
p' - q' <> 0. (TOP-REAL 2) by A1, EUCLID:47;
then |.(p' - q').| <> 0 by EUCLID_2:64;
then reconsider r = |.(p' - q').| as positive Real ;
consider ap being Point of , Up being open Subset of such that
A4: p in Up and
ap in Up and
A5: for b being Point of st b in Up holds
|.(b - ap).| < r / 2 by Th34;
consider aq being Point of , Uq being open Subset of such that
A6: q in Uq and
aq in Uq and
A7: for b being Point of 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 A4; :: 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 A8: |.(q' - ap).| < r / 2 by A5;
|.(q' - ap).| = |.(ap - q').| by TOPRNS_1:28;
then |.(p' - ap).| + |.(ap - q').| < (r / 2) + (r / 2) by A8, A4, A5, XREAL_1:10;
hence contradiction by TOPRNS_1:35; :: thesis: verum

end;

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