let x, y be real number ; for r being real positive number st r <= y holds
Ball |[x,y]|,r is open Subset of Niemytzki-plane
let r be real positive number ; ( 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
set ;
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 &
abs (y - (z `2 )) = y - (z `2 ) ) )
by A1, ABSVALUE:def 1, XREAL_1:48;
A5:
z = |[(z `1 ),(z `2 )]|
by EUCLID:57;
then A6:
z - |[x,y]| = |[((z `1 ) - x),((z `2 ) - y)]|
by EUCLID:66;
then A7:
(z - |[x,y]|) `2 = (z `2 ) - y
by EUCLID:56;
(z - |[x,y]|) `1 = (z `1 ) - x
by A6, EUCLID:56;
then
|.(z - |[x,y]|).| = sqrt ((((z `1 ) - x) ^2 ) + (((z `2 ) - y) ^2 ))
by A7, JGRAPH_1:47;
then
|.(z - |[x,y]|).| >= abs ((z `2 ) - y)
by COMPLEX1:165;
then A8:
|.(z - |[x,y]|).| >= abs (y - (z `2 ))
by COMPLEX1:146;
|.(z - |[x,y]|).| < r
by A3, TOPREAL9:7;
then
abs (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, Th32;
hence
Ball |[x,y]|,r is open Subset of Niemytzki-plane
by A2, XBOOLE_1:28; verum