set X = Niemytzki-plane ;
let x, y be Point of Niemytzki-plane; URYSOHN1:def 7 ( x = y or ex b1, b2 being Element of bool the carrier of Niemytzki-plane st
( b1 is open & b2 is open & x in b1 & not y in b1 & y in b2 & not x in b2 ) )
A1:
the carrier of Niemytzki-plane = y>=0-plane
by Def3;
then A2:
y in y>=0-plane
;
x in y>=0-plane
by A1;
then reconsider a = x, b = y as Point of (TOP-REAL 2) by A2;
assume
x <> y
; ex b1, b2 being Element of bool the carrier of Niemytzki-plane st
( b1 is open & b2 is open & x in b1 & not y in b1 & y in b2 & not x in b2 )
then
|.(a - b).| <> 0
by TOPRNS_1:28;
then reconsider r = |.(a - b).| as positive Real ;
consider q being Point of (TOP-REAL 2), U being open Subset of Niemytzki-plane such that
A3:
x in U
and
q in U
and
A4:
for c being Point of (TOP-REAL 2) st c in U holds
|.(c - q).| < r / 2
by Th30;
consider p being Point of (TOP-REAL 2), V being open Subset of Niemytzki-plane such that
A5:
y in V
and
p in V
and
A6:
for c being Point of (TOP-REAL 2) st c in V holds
|.(c - p).| < r / 2
by Th30;
take
U
; ex b1 being Element of bool the carrier of Niemytzki-plane st
( U is open & b1 is open & x in U & not y in U & y in b1 & not x in b1 )
take
V
; ( 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 A3; ( not y in U & y in V & not x in V )
hereby ( y in V & not x in V )
end;
thus
y in V
by A5; not x in V
assume A8:
x in V
; contradiction
A9:
|.(a - b).| <= |.(a - p).| + |.(p - b).|
by TOPRNS_1:34;
|.(b - p).| < r / 2
by A5, A6;
then
|.(a - p).| + |.(b - p).| < (r / 2) + (r / 2)
by A8, A6, XREAL_1:8;
hence
contradiction
by A9, TOPRNS_1:27; verum