deffunc H₁( Point of (TOP-REAL 2)) -> Element of omega = 1;
deffunc H₂( Point of (TOP-REAL 2)) -> set = |.(|[x,y]| - $1).| / r;
defpred S₁[ set ] means not $1 in Ball (|[x,y]|,r);
A1: for a being Point of (TOP-REAL 2) st a in the carrier of Niemytzki-plane holds
( ( S₁[a] implies H₁(a) in the carrier of I[01] ) & ( not S₁[a] implies H₂(a) in the carrier of I[01] ) )

proof

let a be Point of (TOP-REAL 2); :: thesis: ( a in the carrier of Niemytzki-plane implies ( ( S₁[a] implies H₁(a) in the carrier of I[01] ) & ( not S₁[a] implies H₂(a) in the carrier of I[01] ) ) )
assume a in the carrier of Niemytzki-plane ; :: thesis: ( ( S₁[a] implies H₁(a) in the carrier of I[01] ) & ( not S₁[a] implies H₂(a) in the carrier of I[01] ) )
thus ( S₁[a] implies H₁(a) in the carrier of I[01] ) by BORSUK_1:40, XXREAL_1:1; :: thesis: ( not S₁[a] implies H₂(a) in the carrier of I[01] )
assume not S₁[a] ; :: thesis: H₂(a) in the carrier of I[01]
then |.(a - |[x,y]|).| < r by TOPREAL9:7;
then |.(|[x,y]| - a).| < r by TOPRNS_1:27;
then A2: H₂(a) < r / r by XREAL_1:74;
r / r = 1 by XCMPLX_1:60;
hence H₂(a) in the carrier of I[01] by A2, BORSUK_1:40, XXREAL_1:1; :: thesis: verum

end;

the carrier of Niemytzki-plane = y>=0-plane by Def3;
then A3: the carrier of Niemytzki-plane c= the carrier of (TOP-REAL 2) ;
consider f being Function of Niemytzki-plane,I[01] such that
A4: for a being Point of (TOP-REAL 2) st a in the carrier of Niemytzki-plane holds
( ( S₁[a] implies f . a = H₁(a) ) & ( not S₁[a] implies f . a = H₂(a) ) ) from TOPGEN_5:sch 1(A3, A1);
take f ; :: thesis: for a being Real
for b being non negative Real holds
( ( not |[a,b]| in Ball (|[x,y]|,r) implies f . |[a,b]| = 1 ) & ( |[a,b]| in Ball (|[x,y]|,r) implies f . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) )
let a be Real; :: thesis: for b being non negative Real holds
( ( not |[a,b]| in Ball (|[x,y]|,r) implies f . |[a,b]| = 1 ) & ( |[a,b]| in Ball (|[x,y]|,r) implies f . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) )
let b be non negative Real; :: thesis: ( ( not |[a,b]| in Ball (|[x,y]|,r) implies f . |[a,b]| = 1 ) & ( |[a,b]| in Ball (|[x,y]|,r) implies f . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) )
|[a,b]| in the carrier of Niemytzki-plane by Lm1;
hence ( ( not |[a,b]| in Ball (|[x,y]|,r) implies f . |[a,b]| = 1 ) & ( |[a,b]| in Ball (|[x,y]|,r) implies f . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) ) by A4; :: thesis: verum