let x, y be real number ; :: thesis: 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 ; :: 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
then A2:
(Ball |[x,y]|,r) /\ y>=0-plane is open Subset of Niemytzki-plane
by Th32;
Ball |[x,y]|,r c= y>=0-plane
proof
let a be
set ;
:: 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 = |[(z `1 ),(z `2 )]|
by EUCLID:57;
then
z - |[x,y]| = |[((z `1 ) - x),((z `2 ) - y)]|
by EUCLID:66;
then
(
(z - |[x,y]|) `1 = (z `1 ) - x &
(z - |[x,y]|) `2 = (z `2 ) - y )
by EUCLID:56;
then
(
(z `1 ) - x is
Real &
(z `2 ) - y is
Real &
|.(z - |[x,y]|).| = sqrt ((((z `1 ) - x) ^2 ) + (((z `2 ) - y) ^2 )) )
by JGRAPH_1:47;
then
|.(z - |[x,y]|).| >= abs ((z `2 ) - y)
by COMPLEX1:165;
then
(
|.(z - |[x,y]|).| >= abs (y - (z `2 )) &
|.(z - |[x,y]|).| < r )
by A3, COMPLEX1:146, TOPREAL9:7;
then A5:
abs (y - (z `2 )) < r
by XXREAL_0:2;
(
z `2 < 0 implies (
y - (z `2 ) > y &
abs (y - (z `2 )) = y - (z `2 ) ) )
by A1, ABSVALUE:def 1, XREAL_1:48;
hence
a in y>=0-plane
by A1, A4, A5, XXREAL_0:2;
:: thesis: verum
end;
hence
Ball |[x,y]|,r is open Subset of Niemytzki-plane
by A2, XBOOLE_1:28; :: thesis: verum