set T = Niemytzki-plane ;
let p, q be Point of Niemytzki-plane; :: according to URYSOHN1:def 7 :: thesis: ( p = q or ex b1, b2 being Element of bool the carrier of Niemytzki-plane st
( b1 is open & b2 is open & p in b1 & not q in b1 & q in b2 & not p in b2 ) )
assume A1: p <> q ; :: thesis: ex b1, b2 being Element of bool the carrier of Niemytzki-plane st
( b1 is open & b2 is open & p in b1 & not q in b1 & q in b2 & not p in b2 )
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 p9 = p, q9 = q as Point of (TOP-REAL 2) by A2, A3;
p9 - q9 <> 0. (TOP-REAL 2) by A1, RLVECT_1:21;
then |.(p9 - q9).| <> 0 by EUCLID_2:42;
then reconsider r = |.(p9 - q9).| as positive Real ;
consider ap being Point of (TOP-REAL 2), Up being open Subset of Niemytzki-plane such that
A4: p in Up and
ap in Up and
A5: for b being Point of (TOP-REAL 2) st b in Up holds
|.(b - ap).| < r / 2 by Th30;
consider aq being Point of (TOP-REAL 2), Uq being open Subset of Niemytzki-plane such that
A6: q in Uq and
aq in Uq and
A7: for b being Point of (TOP-REAL 2) st b in Uq holds
|.(b - aq).| < r / 2 by Th30;
take Up ; :: thesis: ex b1 being Element of bool the carrier of Niemytzki-plane st
( Up is open & b1 is open & p in Up & not q in Up & q in b1 & not p in b1 )
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: |.(q9 - ap).| < r / 2 by A5;
|.(q9 - ap).| = |.(ap - q9).| by TOPRNS_1:27;
then |.(p9 - ap).| + |.(ap - q9).| < (r / 2) + (r / 2) by A8, A4, A5, XREAL_1:8;
hence contradiction by TOPRNS_1:34; :: thesis: verum
end;
thus q in Uq by A6; :: thesis: not p in Uq
assume A9: p in Uq ; :: thesis: contradiction
A10: |.(q9 - aq).| = |.(aq - q9).| by TOPRNS_1:27;
|.(q9 - aq).| < r / 2 by A6, A7;
then |.(p9 - aq).| + |.(aq - q9).| < (r / 2) + (r / 2) by A10, A9, A7, XREAL_1:8;
hence contradiction by TOPRNS_1:34; :: thesis: verum