let x, y be Real; for r being positive Real st r <= y holds
Ball (|[x,y]|,r) is open Subset of Niemytzki-plane
let r be positive Real; ( r <= y implies Ball (|[x,y]|,r) is open Subset of Niemytzki-plane )
assume A1:
r <= y
; Ball (|[x,y]|,r) is open Subset of Niemytzki-plane
A2:
Ball (|[x,y]|,r) c= y>=0-plane
proof
let a be
object ;
TARSKI:def 3 ( not a in Ball (|[x,y]|,r) or a in y>=0-plane )
assume A3:
a in Ball (
|[x,y]|,
r)
;
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;
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; verum