deffunc H1( Point of (TOP-REAL 2)) -> set = (|.(|[x,0]| - $1).| ^2) / ((2 * r) * ($1 `2));
deffunc H2( Point of (TOP-REAL 2)) -> Element of omega = 1;
deffunc H3( Point of (TOP-REAL 2)) -> Element of omega = 0 ;
defpred S1[ set ] means not $1 in Ball (|[x,r]|,r);
defpred S2[ set ] means $1 = |[x,0]|;
A1: for a being Point of (TOP-REAL 2) st a in the carrier of Niemytzki-plane holds
( ( S2[a] implies H3(a) in the carrier of I[01] ) & ( not S2[a] & S1[a] implies H2(a) in the carrier of I[01] ) & ( not S2[a] & not S1[a] implies H1(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 ( ( S2[a] implies H3(a) in the carrier of I[01] ) & ( not S2[a] & S1[a] implies H2(a) in the carrier of I[01] ) & ( not S2[a] & not S1[a] implies H1(a) in the carrier of I[01] ) ) )
assume a in the carrier of Niemytzki-plane ; :: thesis: ( ( S2[a] implies H3(a) in the carrier of I[01] ) & ( not S2[a] & S1[a] implies H2(a) in the carrier of I[01] ) & ( not S2[a] & not S1[a] implies H1(a) in the carrier of I[01] ) )
thus ( S2[a] implies H3(a) in the carrier of I[01] ) by BORSUK_1:40, XXREAL_1:1; :: thesis: ( ( not S2[a] & S1[a] implies H2(a) in the carrier of I[01] ) & ( not S2[a] & not S1[a] implies H1(a) in the carrier of I[01] ) )
thus ( not S2[a] & S1[a] implies H2(a) in the carrier of I[01] ) by BORSUK_1:40, XXREAL_1:1; :: thesis: ( not S2[a] & not S1[a] implies H1(a) in the carrier of I[01] )
assume not S2[a] ; :: thesis: ( S1[a] or H1(a) in the carrier of I[01] )
A2: a = |[(a `1),(a `2)]| by EUCLID:53;
assume not S1[a] ; :: thesis: H1(a) in the carrier of I[01]
then |.(a - |[x,r]|).| < r by TOPREAL9:7;
then |.|[((a `1) - x),((a `2) - r)]|.| < r by A2, EUCLID:62;
then A3: |.|[((a `1) - x),((a `2) - r)]|.| ^2 < r ^2 by SQUARE_1:16;
A4: |[((a `1) - x),((a `2) - r)]| `2 = (a `2) - r by EUCLID:52;
|[((a `1) - x),((a `2) - r)]| `1 = (a `1) - x by EUCLID:52;
then (((a `1) - x) ^2) + (((a `2) - r) ^2) < r ^2 by A4, A3, JGRAPH_1:29;
then ((((a `1) - x) ^2) + (((a `2) ^2) - ((2 * (a `2)) * r))) + (r ^2) < 0 + (r ^2) ;
then ((((a `1) - x) ^2) + ((a `2) ^2)) - ((2 * (a `2)) * r) < 0 by XREAL_1:6;
then A5: (((a `1) - x) ^2) + (((a `2) - 0) ^2) < (2 * r) * (a `2) by XREAL_1:48;
A6: |[((a `1) - x),(a `2)]| `2 = a `2 by EUCLID:52;
|[((a `1) - x),(a `2)]| `1 = (a `1) - x by EUCLID:52;
then A7: |.|[((a `1) - x),((a `2) - 0)]|.| ^2 < (2 * r) * (a `2) by A6, A5, JGRAPH_1:29;
then |.(a - |[x,0]|).| ^2 < (2 * r) * (a `2) by A2, EUCLID:62;
then |.(|[x,0]| - a).| ^2 < (2 * r) * (a `2) by TOPRNS_1:27;
then H1(a) <= 1 by XREAL_1:183;
hence H1(a) in the carrier of I[01] by A7, BORSUK_1:40, XXREAL_1:1; :: thesis: verum
end;
the carrier of Niemytzki-plane = y>=0-plane by Def3;
then A8: the carrier of Niemytzki-plane c= the carrier of (TOP-REAL 2) ;
consider f being Function of Niemytzki-plane,I[01] such that
A9: for a being Point of (TOP-REAL 2) st a in the carrier of Niemytzki-plane holds
( ( S2[a] implies f . a = H3(a) ) & ( not S2[a] & S1[a] implies f . a = H2(a) ) & ( not S2[a] & not S1[a] implies f . a = H1(a) ) ) from TOPGEN_5:sch 2(A8, A1);
 take f ; :: thesis: ( f . |[x,0]| = 0 & ( for a being Real
for b being non negative Real holds
( ( ( a <> x or b <> 0 ) & not |[a,b]| in Ball (|[x,r]|,r) implies f . |[a,b]| = 1 ) & ( |[a,b]| in Ball (|[x,r]|,r) implies f . |[a,b]| = (|.(|[x,0]| - |[a,b]|).| ^2) / ((2 * r) * b) ) ) ) )
A10: the carrier of Niemytzki-plane = y>=0-plane by Def3;
then |[x,0]| in the carrier of Niemytzki-plane ;
hence f . |[x,0]| = 0 by A9; :: thesis: for a being Real
for b being non negative Real holds
( ( ( a <> x or b <> 0 ) & not |[a,b]| in Ball (|[x,r]|,r) implies f . |[a,b]| = 1 ) & ( |[a,b]| in Ball (|[x,r]|,r) implies f . |[a,b]| = (|.(|[x,0]| - |[a,b]|).| ^2) / ((2 * r) * b) ) )
let a be Real; :: thesis: for b being non negative Real holds
( ( ( a <> x or b <> 0 ) & not |[a,b]| in Ball (|[x,r]|,r) implies f . |[a,b]| = 1 ) & ( |[a,b]| in Ball (|[x,r]|,r) implies f . |[a,b]| = (|.(|[x,0]| - |[a,b]|).| ^2) / ((2 * r) * b) ) )
let b be non negative Real; :: thesis: ( ( ( a <> x or b <> 0 ) & not |[a,b]| in Ball (|[x,r]|,r) implies f . |[a,b]| = 1 ) & ( |[a,b]| in Ball (|[x,r]|,r) implies f . |[a,b]| = (|.(|[x,0]| - |[a,b]|).| ^2) / ((2 * r) * b) ) )
A11: |[a,b]| in the carrier of Niemytzki-plane by A10;
hereby :: thesis: ( |[a,b]| in Ball (|[x,r]|,r) implies f . |[a,b]| = (|.(|[x,0]| - |[a,b]|).| ^2) / ((2 * r) * b) )
assume ( a <> x or b <> 0 ) ; :: thesis: ( not |[a,b]| in Ball (|[x,r]|,r) implies f . |[a,b]| = 1 )
then not S2[|[a,b]|] by SPPOL_2:1;
hence ( not |[a,b]| in Ball (|[x,r]|,r) implies f . |[a,b]| = 1 ) by A9, A11; :: thesis: verum
end;
assume A12: |[a,b]| in Ball (|[x,r]|,r) ; :: thesis: f . |[a,b]| = (|.(|[x,0]| - |[a,b]|).| ^2) / ((2 * r) * b)
A13: |[x,0]| in y=0-line ;
A14: |[a,b]| `2 = b by EUCLID:52;
Ball (|[x,r]|,r) misses y=0-line by Th21;
then not S2[|[a,b]|] by A13, A12, XBOOLE_0:3;
hence f . |[a,b]| = (|.(|[x,0]| - |[a,b]|).| ^2) / ((2 * r) * b) by A14, A9, A11, A12; :: thesis: verum