let x, y be Real; :: thesis: for r being positive Real st r <= y holds
Ball (|[x,y]|,r) is open Subset of Niemytzki-plane
let r be positive Real; :: thesis: ( r <= y implies Ball (|[x,y]|,r) is open Subset of Niemytzki-plane )
assume A1: r <= y ; :: thesis: Ball (|[x,y]|,r) is open Subset of Niemytzki-plane
A2: Ball (|[x,y]|,r) c= y>=0-plane

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Ball (|[x,y]|,r) or a in y>=0-plane )
assume A3: a in Ball (|[x,y]|,r) ; :: thesis: a in y>=0-plane
then reconsider z = a as Element of (TOP-REAL 2) ;
A4: ( z `2 < 0 implies ( y - (z `2) > y & |.(y - (z `2)).| = y - (z `2) ) ) by A1, ABSVALUE:def 1, XREAL_1:46;
A5: z = |[(z `1),(z `2)]| by EUCLID:53;
then A6: z - |[x,y]| = |[((z `1) - x),((z `2) - y)]| by EUCLID:62;
then A7: (z - |[x,y]|) `2 = (z `2) - y by EUCLID:52;
(z - |[x,y]|) `1 = (z `1) - x by A6, EUCLID:52;
then |.(z - |[x,y]|).| = sqrt ((((z `1) - x) ^2) + (((z `2) - y) ^2)) by A7, JGRAPH_1:30;
then |.(z - |[x,y]|).| >= |.((z `2) - y).| by COMPLEX1:79;
then A8: |.(z - |[x,y]|).| >= |.(y - (z `2)).| by COMPLEX1:60;
|.(z - |[x,y]|).| < r by A3, TOPREAL9:7;
then |.(y - (z `2)).| < r by A8, XXREAL_0:2;
hence a in y>=0-plane by A4, A1, A5, XXREAL_0:2; :: thesis: verum

end;

(Ball (|[x,y]|,r)) /\ y>=0-plane is open Subset of Niemytzki-plane by A1, Th28;
hence Ball (|[x,y]|,r) is open Subset of Niemytzki-plane by A2, XBOOLE_1:28; :: thesis: verum