let a be Point of Niemytzki-plane; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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; :: thesis: ( a in B & B c= A )
thus a in B by A7, YELLOW_8:12; :: thesis: 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; :: thesis: verum