consider BB being Neighborhood_System of Niemytzki-plane such that
for x being Real holds BB . |[x,0]| = { ((Ball (|[x,r]|,r)) \/ {|[x,0]|}) where r is Real : r > 0 }
and
A1:
for x, y being Real st y > 0 holds
BB . |[x,y]| = { ((Ball (|[x,y]|,r)) /\ y>=0-plane) where r is Real : r > 0 }
by Def3;
A2:
the carrier of Niemytzki-plane = y>=0-plane
by Def3;
then reconsider A = y>=0-plane \ y=0-line as Subset of Niemytzki-plane by XBOOLE_1:36;
now for a being Point of Niemytzki-plane st a in A holds
ex B being Subset of Niemytzki-plane st
( B in Union BB & a in B & B c= A )let a be
Point of
Niemytzki-plane;
( a in A implies ex B being Subset of Niemytzki-plane st
( B in Union BB & a in B & B c= A ) )assume A3:
a in A
;
ex B being Subset of Niemytzki-plane st
( B in Union BB & a in B & B c= A )then
a in y>=0-plane
by XBOOLE_0:def 5;
then consider x,
y being
Real such that A4:
a = |[x,y]|
and A5:
y >= 0
;
set B =
(Ball (|[x,y]|,y)) /\ y>=0-plane;
reconsider B =
(Ball (|[x,y]|,y)) /\ y>=0-plane as
Subset of
Niemytzki-plane by A2, XBOOLE_1:17;
not
a in y=0-line
by A3, XBOOLE_0:def 5;
then A6:
y <> 0
by A4;
then
B in { ((Ball (|[x,y]|,r)) /\ y>=0-plane) where r is Real : r > 0 }
by A5;
then A7:
B in BB . a
by A1, A4, A5, A6;
take B =
B;
( B in Union BB & a in B & B c= A )
dom BB = the
carrier of
Niemytzki-plane
by PARTFUN1:def 2;
hence
B in Union BB
by A7, CARD_5:2;
( a in B & B c= A )thus
a in B
by A7, YELLOW_8:12;
B c= A
Ball (
|[x,y]|,
y)
c= y>=0-plane
by A5, A6, Th20;
then
B = Ball (
|[x,y]|,
y)
by XBOOLE_1:28;
then
B misses y=0-line
by A5, A6, Th21;
hence
B c= A
by A2, XBOOLE_1:86;
verum end;
hence
y>=0-plane \ y=0-line is open Subset of Niemytzki-plane
by YELLOW_9:31; verum