:: Niemytzki Plane -- an Example of {T}ychonoff Space Which Is Not $T_4$
::  by Grzegorz Bancerek

environ

 vocabularies NUMBERS, SUBSET_1, XXREAL_0, ORDINAL1, FUNCT_1, PARTFUN1,
      FUNCT_4, RELAT_1, XBOOLE_0, TARSKI, FUNCT_6, FUNCOP_1, FUNCT_2, FUNCT_5,
      ZFMISC_1, MCART_1, CARD_3, FINSEQ_1, CARD_1, CARD_2, COMPLEX1, EUCLID,
      SQUARE_1, ARYTM_3, PRE_TOPC, RCOMP_1, ORDINAL2, STRUCT_0, METRIC_1,
      ARYTM_1, SUPINF_2, REAL_1, TOPGEN_3, TOPGEN_2, CANTOR_1, PBOOLE,
      SETFAM_1, RAT_1, TOPS_1, TOPGEN_1, XXREAL_1, RLVECT_3, BORSUK_1, CARD_5,
      TOPMETR, TOPS_2, VALUED_1, FINSET_1, LIMFUNC1, TOPGEN_5, FUNCT_7;
 notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, RELAT_1, FINSET_1, SUBSET_1,
      MCART_1, SETFAM_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1,
      FINSEQ_1, FUNCT_4, FUNCOP_1, PBOOLE, ORDINAL1, CARD_1, CARD_2, CARD_3,
      FUNCT_5, FUNCT_6, NUMBERS, XCMPLX_0, SQUARE_1, COMPLEX1, REAL_1, XREAL_0,
      XXREAL_2, RAT_1, RCOMP_1, LIMFUNC1, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_1,
      TOPS_2, RLVECT_1, EUCLID, CANTOR_1, TOPMETR, TOPREAL9, TOPGEN_1,
      TOPGEN_2, TOPGEN_3, XXREAL_0;
 constructors WELLORD2, FUNCT_4, REAL_1, SQUARE_1, COMPLEX1, CARD_2, PROB_1,
      RCOMP_1, LIMFUNC1, FUNCT_6, TOPS_1, MONOID_0, BORSUK_4, TOPGEN_2,
      TOPREAL9, TOPGEN_1, TOPGEN_3, XXREAL_2, BINOP_2, XTUPLE_0, BINOP_1;
 registrations SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, FINSET_1,
      NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1, RAT_1, CARD_1, MEMBERED,
      FINSEQ_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, MONOID_0, EUCLID,
      TOPMETR, TOPGRP_1, TOPGEN_1, VALUED_0, XXREAL_2, RELSET_1, XTUPLE_0,
      REAL_1, ORDINAL1;
 requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
 definitions TARSKI, XBOOLE_0, FUNCT_1, PARTFUN1, FUNCOP_1, WELLORD2, PBOOLE,
      PRE_TOPC, TOPS_3, URYSOHN1, TOPGEN_1, COMPTS_1;
 equalities RELAT_1, XBOOLE_0, FUNCOP_1, FUNCT_6, BINOP_1, SQUARE_1, SUBSET_1,
      STRUCT_0, LIMFUNC1, PROB_1, ORDINAL1, RLVECT_1;
 expansions RELAT_1, TARSKI, XBOOLE_0, PBOOLE, PRE_TOPC, TOPGEN_1;
 theorems TOPS_3, TARSKI, XBOOLE_0, XBOOLE_1, ZFMISC_1, FUNCT_1, EUCLID,
      PBOOLE, EUCLID_2, TOPREAL9, TOPGEN_3, SETWISEO, XREAL_1, XREAL_0,
      XCMPLX_1, TOPRNS_1, TOPREAL6, ABSVALUE, SPPOL_2, FINSEQ_1, COMPLEX1,
      JGRAPH_1, YELLOW_9, NUMBERS, CARD_5, TOPGEN_2, SUBSET_1, YELLOW_8,
      TOPS_1, PRE_TOPC, TOPGEN_1, SQUARE_1, RAT_1, CARD_1, CARD_2, CARD_3,
      CARD_4, FINSEQ_3, MCART_1, FUNCT_6, BORSUK_1, TOPALG_1, TOPS_2, FUNCT_2,
      TIETZE, JGRAPH_5, URYSOHN1, TOPMETR, BOOLMARK, FUNCOP_1, FUNCT_4,
      RELAT_1, RELSET_1, CANTOR_1, PARTFUN1, SETFAM_1, JORDAN6, YELLOW12,
      FUNCT_7, DICKSON, FUNCT_5, FRECHET, TSP_1, JORDAN, XXREAL_0, TSEP_1,
      XXREAL_1, XXREAL_2, XTUPLE_0, RLVECT_1;
 schemes SUBSET_1, FUNCT_1, PRE_CIRC, FUNCT_5, CLASSES1, FINSET_1, FUNCT_2;

begin :: Preliminaries

reserve x,y for Real,
  u,v,w for set,
  r for positive Real;

theorem Th1:
  for f,g being Function st f tolerates g for A being set holds (f
  +*g)"A = (f"A)\/(g"A)
proof
  let f,g be Function;
  assume
A1: f tolerates g;
  let A be set;
  f c= f+*g by A1,FUNCT_4:28;
  then
A2: f"A c= (f+*g)"A by RELAT_1:144;
  thus (f+*g)"A c= (f"A)\/(g"A)
  proof
    let x be object;
    assume
A3: x in (f+*g)"A;
    then x in dom (f+*g) by FUNCT_1:def 7;
    then x in dom f \/ dom g by FUNCT_4:def 1;
    then x in dom f or x in dom g by XBOOLE_0:def 3;
    then
A4: x in dom f & (f+*g).x = f.x or x in dom g & (f+*g).x = g.x by A1,FUNCT_4:13
,15;
    (f+*g).x in A by A3,FUNCT_1:def 7;
    then x in f"A or x in g"A by A4,FUNCT_1:def 7;
    hence thesis by XBOOLE_0:def 3;
  end;
  g"A c= (f+*g)"A by FUNCT_4:25,RELAT_1:144;
  hence thesis by A2,XBOOLE_1:8;
end;

theorem
  for f,g being Function st dom f misses dom g for A being set holds (f
  +*g)"A = (f"A)\/(g"A) by Th1,PARTFUN1:56;

theorem Th3:
  for x,a being set, f being Function st a in dom f holds (commute
  (x .--> f)).a = x .--> f.a
proof
  let x,a be set;
  let f be Function;
  set g = x .--> f;
A1: dom g = {x};
A2: f in Funcs(dom f, rng f) by FUNCT_2:def 2;
  rng g = {f} by FUNCOP_1:8;
  then rng g c= Funcs(dom f, rng f) by A2,ZFMISC_1:31;
  then
A3: g in Funcs({x}, Funcs(dom f, rng f)) by A1,FUNCT_2:def 2;
A4: g.x = f by FUNCOP_1:72;
A5: x in {x} by TARSKI:def 1;
  assume
A6: a in dom f;
  then
A7: (commute g).a.x = f.a by A3,A4,A5,FUNCT_6:56;
  dom ((commute g).a) = {x} by A3,A6,A4,A5,FUNCT_6:56;
  hence thesis by A7,DICKSON:1;
end;

theorem
  for b being set, f being Function holds b in dom commute f iff ex a
  being set, g being Function st a in dom f & g = f.a & b in dom g
proof
  let b be set;
  let f be Function;
A1: dom commute f = proj2 dom uncurry f by FUNCT_5:23;
  hereby
    assume b in dom commute f;
    then consider a being object such that
A2: [a,b] in dom uncurry f by A1,XTUPLE_0:def 13;
    consider a9 being object, g being Function, b9 being object such that
A3: [a,b] = [a9,b9] and
A4: a9 in dom f and
A5: g = f.a9 and
A6: b9 in dom g by A2,FUNCT_5:def 2;
     reconsider a as set by TARSKI:1;
    take a, g;
    thus a in dom f & g = f.a & b in dom g by A3,A4,A5,A6,XTUPLE_0:1;
  end;
  given a being set, g being Function such that
A7: a in dom f and
A8: g = f.a and
A9: b in dom g;
  [a,b] in dom uncurry f by A7,A8,A9,FUNCT_5:def 2;
  hence thesis by A1,XTUPLE_0:def 13;
end;

theorem Th5:
  for a,b being set, f being Function holds a in dom ((commute f).b
  ) iff ex g being Function st a in dom f & g = f.a & b in dom g
proof
  let a,b be set;
  let f be Function;
  dom uncurry f c= [:dom f, proj1 union rng f:]
  proof
    let u be object;
    assume u in dom uncurry f;
    then consider a being object, g being Function, b being object such that
A1: u = [a,b] and
A2: a in dom f and
A3: g = f.a and
A4: b in dom g by FUNCT_5:def 2;
    g in rng f by A2,A3,FUNCT_1:def 3;
    then g c= union rng f by ZFMISC_1:74;
    then proj1 g c= proj1 union rng f by XTUPLE_0:8;
    hence thesis by A1,A2,A4,ZFMISC_1:def 2;
  end;
  then
A5: uncurry' commute f = uncurry f by FUNCT_5:50;
  hereby
    assume
A6: a in dom ((commute f).b);
    then b in dom commute f by FUNCT_1:def 2,RELAT_1:38;
    then [a,b] in dom uncurry f by A5,A6,FUNCT_5:39;
    then consider a9 being object, g being Function, b9 being object
    such that
A7: [a,b] = [a9,b9] and
A8: a9 in dom f and
A9: g = f.a9 and
A10: b9 in dom g by FUNCT_5:def 2;
    take g;
    thus a in dom f & g = f.a & b in dom g by A7,A8,A9,A10,XTUPLE_0:1;
  end;
  given g being Function such that
A11: a in dom f and
A12: g = f.a and
A13: b in dom g;
  [a,b] in dom uncurry f by A11,A12,A13,FUNCT_5:def 2;
  hence thesis by FUNCT_5:22;
end;

theorem Th6:
  for a,b being set, f,g being Function st a in dom f & g = f.a & b
  in dom g holds (commute f).b.a = g.b
proof
  let a,b be set;
  let f,g be Function;
  assume that
A1: a in dom f and
A2: g = f.a and
A3: b in dom g;
A4: [a,b] in dom uncurry f by A1,A2,A3,FUNCT_5:def 2;
A5: [a,b]`2 = b;
  [a,b]`1 = a;
  then (uncurry f).(a,b) = g.b by A5,A4,A2,FUNCT_5:def 2;
  hence thesis by A4,FUNCT_5:22;
end;

theorem Th7:
  for a being set, f,g,h being Function st h = f \/ g holds (
  commute h).a = (commute f).a \/ (commute g).a
proof
  let a be set;
  let f,g,h be Function;
  assume
A1: h = f \/ g;
  now
    let u,v be object;
    hereby
      assume
A2:   [u,v] in (commute h).a;
      then
A3:   (commute h).a.u = v by FUNCT_1:1;
      u in dom ((commute h).a) by A2,FUNCT_1:1;
      then consider k being Function such that
A4:   u in dom h and
A5:   k = h.u and
A6:   a in dom k by Th5;
      [u,k] in h by A4,A5,FUNCT_1:def 2;
      then [u,k] in f or [u,k] in g by A1,XBOOLE_0:def 3;
      then u in dom f & k = f.u or u in dom g & k = g.u by FUNCT_1:1;
      then
A7:   u in dom ((commute f).a) & (commute f).a.u = k.a or u in dom ((
      commute g).a) & (commute g).a.u = k.a by A6,Th5,Th6;
      (commute h).a.u = k.a by A4,A5,A6,Th6;
      then [u,v] in (commute f).a or [u,v] in (commute g).a by A7,A3,FUNCT_1:1;
      hence [u,v] in (commute f).a \/ (commute g).a by XBOOLE_0:def 3;
    end;
    assume
A8: [u,v] in (commute f).a \/ (commute g).a;
    per cases by A8,XBOOLE_0:def 3;
    suppose
A9:   [u,v] in (commute f).a;
      then
A10:  (commute f).a.u = v by FUNCT_1:1;
      u in dom ((commute f).a) by A9,FUNCT_1:1;
      then consider k being Function such that
A11:  u in dom f and
A12:  k = f.u and
A13:  a in dom k by Th5;
A14:  (commute f).a.u = k.a by A11,A12,A13,Th6;
      [u,k] in f by A11,A12,FUNCT_1:1;
      then
A15:  [u,k] in h by A1,XBOOLE_0:def 3;
      then
A16:  u in dom h by FUNCT_1:1;
A17:  k = h.u by A15,FUNCT_1:1;
      then
A18:  (commute h).a.u = k.a by A16,A13,Th6;
      u in dom ((commute h).a) by A16,A17,A13,Th5;
      hence [u,v] in (commute h).a by A18,A14,A10,FUNCT_1:1;
    end;
    suppose
A19:  [u,v] in (commute g).a;
      then
A20:  (commute g).a.u = v by FUNCT_1:1;
      u in dom ((commute g).a) by A19,FUNCT_1:1;
      then consider k being Function such that
A21:  u in dom g and
A22:  k = g.u and
A23:  a in dom k by Th5;
A24:  (commute g).a.u = k.a by A21,A22,A23,Th6;
      [u,k] in g by A21,A22,FUNCT_1:1;
      then
A25:  [u,k] in h by A1,XBOOLE_0:def 3;
      then
A26:  u in dom h by FUNCT_1:1;
A27:  k = h.u by A25,FUNCT_1:1;
      then
A28:  (commute h).a.u = k.a by A26,A23,Th6;
      u in dom ((commute h).a) by A26,A27,A23,Th5;
      hence [u,v] in (commute h).a by A28,A24,A20,FUNCT_1:1;
    end;
  end;
  hence thesis;
end;

theorem Th8:
  for X,Y being set holds product <*X,Y*>, [:X,Y:] are_equipotent
  & card product <*X,Y*> = (card X)*`(card Y)
proof
  deffunc F(Function) = [$1.1,$1.2];
  let X,Y be set;
  consider f being Function such that
A1: dom f = product <*X,Y*> & for g being Function st g in product <*X,Y
  *> holds f.g = F(g) from FUNCT_5:sch 1;
A2: <*X,Y*>.2 = Y by FINSEQ_1:44;
A3: dom <*X,Y*> = {1,2} by FINSEQ_1:2,89;
A4: <*X,Y*>.1 = X by FINSEQ_1:44;
  thus product <*X,Y*>, [:X,Y:] are_equipotent
  proof
    take f;
    thus f is one-to-one
    proof
      let x1,x2 be object;
      assume that
A5:   x1 in dom f and
A6:   x2 in dom f and
A7:   f.x1 = f.x2;
      consider g2 being Function such that
A8:   x2 = g2 and
A9:   dom g2 = dom <*X,Y*> and
      for y being object st y in dom <*X,Y*> holds g2.y in <*X,Y*>.y by A1,A6,
CARD_3:def 5;
      consider g1 being Function such that
A10:  x1 = g1 and
A11:  dom g1 = dom <*X,Y*> and
      for y being object st y in dom <*X,Y*> holds g1.y in <*X,Y*>.y by A5,A1,
CARD_3:def 5;
A12:  [g1.1,g1.2] = f.x1 by A1,A5,A10
        .= [g2.1,g2.2] by A1,A6,A7,A8;
      now
        let z being object;
        assume z in {1,2};
        then z = 1 or z = 2 by TARSKI:def 2;
        hence g1.z = g2.z by A12,XTUPLE_0:1;
      end;
      hence thesis by A3,A10,A11,A8,A9,FUNCT_1:2;
    end;
    thus dom f = product <*X,Y*> by A1;
    thus rng f c= [:X,Y:]
    proof
      let z be object;
      assume z in rng f;
      then consider t being object such that
A13:  t in dom f and
A14:  z = f.t by FUNCT_1:def 3;
      consider g being Function such that
A15:  t = g and
      dom g = dom <*X,Y*> and
A16:  for y being object st y in dom <*X,Y*> holds g.y in <*X,Y*>.y by A1,A13,
CARD_3:def 5;
      1 in {1,2} by TARSKI:def 2;
      then
A17:  g.1 in X by A3,A4,A16;
      2 in {1,2} by TARSKI:def 2;
      then
A18:  g.2 in Y by A3,A2,A16;
      z = [g.1,g.2] by A1,A13,A14,A15;
      hence thesis by A17,A18,ZFMISC_1:87;
    end;
    let z be object;
    set g = <*z`1,z`2*>;
A19: g.1 = z`1 by FINSEQ_1:44;
A20: g.2 = z`2 by FINSEQ_1:44;
    assume
A21: z in [:X,Y:];
    then
A22: z`2 in Y by MCART_1:10;
    z`1 in X by A21,MCART_1:10;
    then
A23: g in product <*X,Y*> by A22,FINSEQ_3:124;
    z = [z`1,z`2] by A21,MCART_1:21;
    then f.g = z by A23,A1,A19,A20;
    hence thesis by A1,A23,FUNCT_1:def 3;
  end;
  hence card product <*X,Y*> = card [:X,Y:] by CARD_1:5
    .= card [:card X, card Y:] by CARD_2:7
    .= (card X)*`card Y by CARD_2:def 2;
end;

scheme
  SCH1{P[object], A,B,C()-> non empty set, F1,F2(object)-> set}:
ex f being Function
of C(), B() st for a being Element of A() st a in C() holds (P[a] implies f.a =
  F1(a)) & (not P[a] implies f.a = F2(a))
provided
A1: C() c= A() and
A2: for a being Element of A() st a in C() holds (P[a] implies F1(a) in
B()) & (not P[a] implies F2(a) in B())
proof
A3: for a being object st a in C()
    holds (P[a] implies F1(a) in B()) & (not P[a
  ] implies F2(a) in B()) by A1,A2;
  consider f being Function of C(),B() such that
A4: for x being object st x in C() holds (P[ x] implies f.x = F1(x)) & (not
  P[ x] implies f.x = F2(x)) from FUNCT_2:sch 5(A3);
  take f;
  thus thesis by A4;
end;

scheme
  SCH2{P,Q[object], A,B,C()-> non empty set, F1,F2,F3(object)-> object}:
 ex f being
  Function of C(), B() st for a being Element of A() st a in C() holds (P[a]
implies f.a = F1(a)) & (not P[a] & Q[a] implies f.a = F2(a)) & (not P[a] & not
  Q[a] implies f.a = F3(a))
provided
A1: C() c= A() and
A2: for a being Element of A() st a in C() holds (P[a] implies F1(a) in
B()) & (not P[a] & Q[a] implies F2(a) in B()) & (not P[a] & not Q[a] implies F3
(a) in B())
proof
  set D = {a where a is Element of C(): P[a] or Q[a]};
  per cases;
  suppose
A3: D = {};
    consider f being Function such that
A4: dom f = C() &
for u being object st u in C() holds f.u = F3(u) from FUNCT_1:sch
    3;
    rng f c= B()
    proof
      let v be object;
      assume v in rng f;
      then consider u being object such that
A5:   u in dom f and
A6:   v = f.u by FUNCT_1:def 3;
A7:   v = F3(u) by A4,A5,A6;
A8:   not u in D by A3;
      then
A9:   not Q[u] by A4,A5;
      not P[u] by A8,A4,A5;
      hence thesis by A9,A7,A1,A2,A4,A5;
    end;
    then reconsider f as Function of C(), B() by A4,FUNCT_2:2;
    take f;
    let a be Element of A();
    assume
A10: a in C();
    not a in D by A3;
    hence thesis by A4,A10;
  end;
  suppose
    D <> {};
    then reconsider D as non empty set;
    defpred PQ[object] means P[$1] or Q[$1];
A11: for a being object st a in D holds (P[a] implies F1(a) in B()) & (not P[
    a] implies F2(a) in B())
    proof
      let a be object;
      assume a in D;
      then
A12:  ex b being Element of C() st a = b & (P[b] or Q[b]);
      then a in C();
      hence thesis by A12,A1,A2;
    end;
    consider g being Function of D,B() such that
A13: for x being object st x in D holds (P[ x] implies g.x = F1(x)) & (
    not P[ x] implies g.x = F2(x)) from FUNCT_2:sch 5(A11);
    deffunc F12(object) = g.$1;
A14: for a being object st a in C() holds (PQ[a] implies F12(a) in B()) & (
    not PQ[a] implies F3(a) in B())
    proof
      let a be object;
      assume
A15:  a in C();
      hereby
        assume PQ[a];
        then
A16:    a in D by A15;
        then
A17:    not P[a] implies F2(a) in B() by A11;
        P[a] implies F1(a) in B() by A16,A11;
        hence F12(a) in B() by A17,A16,A13;
      end;
      thus thesis by A1,A2,A15;
    end;
    consider f being Function of C(),B() such that
A18: for x being object st x in C() holds (PQ[ x] implies f.x = F12(x)) &
    (not PQ[ x] implies f.x = F3(x)) from FUNCT_2:sch 5(A14);
    take f;
    let a be Element of A();
    assume
A19: a in C();
    then PQ[a] implies f.a = g.a & a in D by A18;
    hence
    (P[a] implies f.a = F1(a)) & (not P[a] & Q[a] implies f.a = F2(a)) by A13;
    thus thesis by A18,A19;
  end;
end;

theorem Th9:
  for a,b being Real holds |.|[a,b]|.|^2 = a^2+b^2
proof
  let a,b be Real;
A1: |[a,b]|`2 = b by EUCLID:52;
  |[a,b]|`1 = a by EUCLID:52;
  hence thesis by A1,JGRAPH_1:29;
end;

theorem Th10:
  for X being TopSpace, Y being non empty TopSpace for A,B being
  closed Subset of X for f being continuous Function of X|A, Y for g being
  continuous Function of X|B, Y st f tolerates g holds f+*g is continuous
  Function of X|(A \/ B), Y
proof
  let X be TopSpace, Y be non empty TopSpace;
  let A,B be closed Subset of X;
  let f be continuous Function of X|A, Y;
  let g be continuous Function of X|B, Y such that
A1: f tolerates g;
A2: the carrier of X|(A \/ B) = A \/ B by PRE_TOPC:8;
  the carrier of X|B = B by PRE_TOPC:8;
  then
A3: dom g = B by FUNCT_2:def 1;
  the carrier of X|A = A by PRE_TOPC:8;
  then
A4: dom f = A by FUNCT_2:def 1;
A5: rng (f+*g) c= rng f \/ rng g by FUNCT_4:17;
  dom (f+*g) = dom f \/ dom g by FUNCT_4:def 1;
  then reconsider h = f+*g as Function of X|(A \/ B), Y by A5,A2,A4,A3,
FUNCT_2:2,XBOOLE_1:1;
  h is continuous
  proof
    let C be Subset of Y;
A6: [#](X|(A \/ B)) = A \/ B by PRE_TOPC:8;
    assume
A7: C is closed;
    then f"C is closed by PRE_TOPC:def 6;
    then consider C1 being Subset of X such that
A8: C1 is closed and
A9: C1 /\ [#](X|A) = f"C by PRE_TOPC:13;
    g"C is closed by A7,PRE_TOPC:def 6;
    then consider C2 being Subset of X such that
A10: C2 is closed and
A11: C2 /\ [#](X|B) = g"C by PRE_TOPC:13;
A12: C1/\A\/C2/\B is closed by A8,A10;
A13: [#](X|A) = A by PRE_TOPC:8;
A14: [#](X|B) = B by PRE_TOPC:8;
    h"C = (f"C)\/(g"C) by A1,Th1
      .= ((f"C)\/(g"C))/\(A\/B) by A13,A14,XBOOLE_1:13,28;
    hence thesis by A12,A9,A11,A6,A13,A14,PRE_TOPC:13;
  end;
  hence thesis;
end;

theorem Th11:
  for X being TopSpace, Y being non empty TopSpace for A,B being
closed Subset of X st A misses B for f being continuous Function of X|A, Y for
g being continuous Function of X|B, Y holds f+*g is continuous Function of X|(A
  \/ B), Y
proof
  let X be TopSpace, Y be non empty TopSpace;
  let A,B be closed Subset of X such that
A1: A misses B;
  let f be continuous Function of X|A, Y;
  let g be continuous Function of X|B, Y;
  the carrier of X|B = B by PRE_TOPC:8;
  then
A2: dom g = B by FUNCT_2:def 1;
  the carrier of X|A = A by PRE_TOPC:8;
  then dom f = A by FUNCT_2:def 1;
  hence thesis by A2,A1,Th10,PARTFUN1:56;
end;

theorem Th12:
  for X being TopSpace, Y being non empty TopSpace for A being
  open closed Subset of X for f being continuous Function of X|A, Y for g being
  continuous Function of X|A`, Y holds f+*g is continuous Function of X, Y
proof
  let X be TopSpace;
  let Y be non empty TopSpace;
  let A be open closed Subset of X;
  let f be continuous Function of X|A, Y;
  let g be continuous Function of X|A`, Y;
  A\/A` = [#]X by PRE_TOPC:2;
  then
A1: X|(A\/A`) = the TopStruct of X by TSEP_1:93;
  A misses A` by XBOOLE_1:79;
  then
A2: f+*g is continuous Function of X|(A\/A`), Y by Th11;
  the TopStruct of Y = the TopStruct of Y;
  hence thesis by A2,A1,YELLOW12:36;
end;

begin :: Niemytzki plane

theorem Th13:
  for n being Element of NAT for a being Point of TOP-REAL n for r
  being positive Real holds a in Ball(a,r)
proof
  let n be Element of NAT;
  let a be Point of TOP-REAL n;
  let r be positive Real;
  a-a = 0.TOP-REAL n by RLVECT_1:5;
  then |.a-a.| = 0 by EUCLID_2:39;
  hence thesis by TOPREAL9:7;
end;

definition
  func y=0-line -> Subset of TOP-REAL 2 equals
  the set of all |[x,0]|;
  coherence
  proof
    set A = the set of all |[x,0]|;
    A c= the carrier of TOP-REAL 2
    proof
      let a be object;
      assume a in A;
      then ex x st a = |[x,0]|;
      hence thesis;
    end;
    hence thesis;
  end;
  func y>=0-plane -> Subset of TOP-REAL 2 equals
  {|[x,y]|: y >= 0};
  coherence
  proof
    set A = {|[x,y]|: y >= 0};
    A c= the carrier of TOP-REAL 2
    proof
      let a be object;
      assume a in A;
      then ex x,y st a = |[x,y]| & y >= 0;
      hence thesis;
    end;
    hence thesis;
  end;
end;

theorem
  for a,b being set holds <*a,b*> in y=0-line iff a in REAL & b = 0
proof
  let a,b be set;
A1: <*a,b*> in y=0-line iff ex x st <*a,b*> = |[x,0]|;
  hereby
A2: <*a,b*>.1 = a by FINSEQ_1:44;
    assume <*a,b*> in y=0-line;
    then consider x,y such that
A3: <*a,b*> = |[x,0]| by A1;
    <*a,b*>.1 = x by A3,FINSEQ_1:44;
    hence a in REAL by A2,XREAL_0:def 1;
    <*a,b*>.2 = b by FINSEQ_1:44;
    hence b = 0 by A3,FINSEQ_1:44;
  end;
  assume a in REAL;
  then reconsider x = a as Real;
  |[x,0]| = <*a,0 *>;
  hence thesis;
end;

theorem Th15:
  for a,b being Real holds |[a,b]| in y=0-line iff b = 0
proof
  let a,b be Real;
  |[a,b]| in y=0-line iff ex x st |[a,b]| = |[x,0]|;
  hence thesis by SPPOL_2:1;
end;

theorem Th16:
  card y=0-line = continuum
proof
  deffunc F(Real) = |[$1,0]|;
  consider f being Function such that
A1: dom f = REAL and
A2: for r being Element of REAL holds f.r = F(r) from FUNCT_1:sch 4;
  REAL, y=0-line are_equipotent
  proof
    take f;
    thus f is one-to-one
    proof
      let x,y be object;
      assume that
A3:   x in dom f and
A4:   y in dom f;
      reconsider x,y as Element of REAL by A3,A4,A1;
A5:   f.y = |[y,0]| by A2;
      f.x = |[x,0]| by A2;
      hence thesis by A5,SPPOL_2:1;
    end;
    thus dom f = REAL by A1;
    thus rng f c= y=0-line
    proof
      let a be object;
      assume a in rng f;
      then consider b being object such that
A6:   b in dom f and
A7:   a = f.b by FUNCT_1:def 3;
      reconsider b as Element of REAL by A1,A6;
      a = |[b,0]| by A2,A7;
      hence thesis;
    end;
    let a be object;
    assume
A8: a in y=0-line;
    then reconsider a as Point of TOP-REAL 2;
    reconsider a1 = a`1 as Element of REAL by XREAL_0:def 1;
A9: a = |[a`1,a`2]| by EUCLID:53;
    then a`2 = 0 by A8,Th15;
    then a = f.a1 by A2,A9;
    hence thesis by A1,FUNCT_1:def 3;
  end;
  hence thesis by CARD_1:5,TOPGEN_3:def 4;
end;

theorem
  for a,b being set holds <*a,b*> in y>=0-plane iff a in REAL & ex y st
  b = y & y >= 0
proof
  let a,b be set;
  hereby
A1: <*a,b*>.1 = a by FINSEQ_1:44;
    assume <*a,b*> in y>=0-plane;
    then consider x,y such that
A2: <*a,b*> = |[x,y]| and
A3: y >= 0;
    <*a,b*>.1 = x by A2,FINSEQ_1:44;
    hence a in REAL by A1,XREAL_0:def 1;
    take y;
    <*a,b*>.2 = b by FINSEQ_1:44;
    hence b = y & y >= 0 by A3,A2,FINSEQ_1:44;
  end;
  assume a in REAL;
  then reconsider x = a as Real;
  given y such that
A4: b = y and
A5: y >= 0;
  |[x,y]| = <*a,b*> by A4;
  hence thesis by A5;
end;

theorem Th18:
  for a,b being Real holds |[a,b]| in y>=0-plane iff b >= 0
proof
  let a,b be Real;
  |[a,b]| in y>=0-plane iff ex x,y st |[a,b]| = |[x,y]| & y >= 0;
  hence thesis by SPPOL_2:1;
end;

registration
  cluster y=0-line -> non empty;
  coherence by Th15;
  cluster y>=0-plane -> non empty;
  coherence by Th18;
end;

theorem Th19:
  y=0-line c= y>=0-plane
proof
  let x be object;
  assume x in y=0-line;
  then reconsider x as Element of y=0-line;
A1: x = |[x`1,x`2]| by EUCLID:53;
  then x`2 = 0 by Th15;
  hence thesis by A1;
end;

theorem Th20:
  for a,b,r being Real st r > 0 holds Ball(|[a,b]|,r) c=
  y>=0-plane iff r <= b
proof
  let a,b,r be Real such that
A1: r > 0;
  hereby
A2: |[a,b]| in Ball(|[a,b]|,r) by A1,Th13;
    assume that
A3: Ball(|[a,b]|,r) c= y>=0-plane and
A4: r > b;
    reconsider b as non negative Real by A2,A3,Th18;
    reconsider br=b-r as negative Real by A4,XREAL_1:49;
    set y = br/2;
    reconsider r as positive Real by A1;
    |[a,y]|-|[a,b]| = |[a-a,y-b]| by EUCLID:62;
    then
A5: |.|[a,y]|-|[a,b]|.| = |.y-b.| by TOPREAL6:23
      .= |.b-y.| by COMPLEX1:60
      .= (b+r)/2 by ABSVALUE:def 1;
    b+r < r+r by A4,XREAL_1:6;
    then (b+r)/2 < (r+r)/2 by XREAL_1:74;
    then |[a,y]| in Ball(|[a,b]|,r) by A5,TOPREAL9:7;
    hence contradiction by A3,Th18;
  end;
  assume
A6: r <= b;
  let x be object;
  assume
A7: x in Ball(|[a,b]|,r);
  then reconsider z = x as Element of TOP-REAL 2;
A8: |.z-|[a,b]|.| < r by A7,TOPREAL9:7;
A9: |[z`1-a,z`2-b]|`1 = z`1-a by EUCLID:52;
A10: |[z`1-a,z`2-b]|`2 = z`2-b by EUCLID:52;
A11: z = |[z`1,z`2]| by EUCLID:53;
  then z-|[a,b]| = |[z`1-a,z`2-b]| by EUCLID:62;
  then |.z-|[a,b]|.| = sqrt((z`1-a)^2+(z`2-b)^2) by A9,A10,JGRAPH_1:30;
  then |.z`2-b.| <= |.z-|[a,b]|.| by COMPLEX1:79;
  then |.z`2-b.| < r by A8,XXREAL_0:2;
  then
A12: |.b-z`2.| < r by COMPLEX1:60;
  now
    assume z`2 < 0;
    then b-z`2 > b by XREAL_1:46;
    then b-z`2 > r by A6,XXREAL_0:2;
    hence contradiction by A1,A12,ABSVALUE:def 1;
  end;
  hence thesis by A11;
end;

theorem Th21:
  for a,b,r being Real st r > 0 & b >= 0 holds Ball(|[a,b]|
  ,r) misses y=0-line iff r <= b
proof
  let a,b,r be Real;
  assume that
A1: r > 0 and
A2: b >= 0;
  hereby
A3: |[a,0]| in y=0-line;
    assume that
A4: Ball(|[a,b]|,r) misses y=0-line and
A5: r > b;
    |[a,0]|-|[a,b]| = |[a-a,0-b]| by EUCLID:62;
    then |.|[a,0]|-|[a,b]|.| = |.0-b.| by TOPREAL6:23
      .= |.b-0 .| by COMPLEX1:60;
    then |.|[a,0]|-|[a,b]|.| < r by A2,A5,ABSVALUE:def 1;
    then |[a,0]| in Ball(|[a,b]|,r) by TOPREAL9:7;
    hence contradiction by A3,A4,XBOOLE_0:3;
  end;
  assume
A6: r <= b;
  assume Ball(|[a,b]|,r) meets y=0-line;
  then consider x being object such that
A7: x in Ball(|[a,b]|,r) and
A8: x in y=0-line by XBOOLE_0:3;
  reconsider x as Element of TOP-REAL 2 by A7;
A9: x = |[x`1,x`2]| by EUCLID:53;
  then x`2 = 0 by A8,Th15;
  then
A10: x-|[a,b]| = |[x`1-a,0-b]| by A9,EUCLID:62;
  then
A11: (x-|[a,b]|)`2 = 0-b by EUCLID:52;
  (x-|[a,b]|)`1 = x`1-a by A10,EUCLID:52;
  then |.x-|[a,b]|.| = sqrt((x`1-a)^2+(0-b)^2) by A11,JGRAPH_1:30;
  then |.x-|[a,b]|.| >= |.0-b.| by COMPLEX1:79;
  then
A12: |.x-|[a,b]|.| >= |.b-0 .| by COMPLEX1:60;
  |.x-|[a,b]|.| < r by A7,TOPREAL9:7;
  then |.b.| < r by A12,XXREAL_0:2;
  hence contradiction by A1,A6,ABSVALUE:def 1;
end;

theorem Th22:
  for n being Element of NAT, a,b being Element of TOP-REAL n, r1,
r2 being positive Real st |.a-b.| <= r1-r2 holds Ball(b,r2) c= Ball(a,
  r1)
proof
  let n be Element of NAT, a,b be Element of TOP-REAL n, r1,r2 be positive
  Real;
  assume |.a-b.| <= r1-r2;
  then
A1: |.b-a.| <= r1-r2 by TOPRNS_1:27;
  let x be object;
  assume
A2: x in Ball(b,r2);
  then reconsider x as Element of TOP-REAL n;
  |.x-b.| < r2 by A2,TOPREAL9:7;
  then
A3: |.x-b.|+|.b-a.| < r2+(r1-r2) by A1,XREAL_1:8;
  |.x-a.| <= |.x-b.|+|.b-a.| by TOPRNS_1:34;
  then |.x-a.| < r2+(r1-r2) by A3,XXREAL_0:2;
  hence thesis by TOPREAL9:7;
end;

theorem Th23:
  for a being Real, r1,r2 being positive Real st
  r1 <= r2 holds Ball(|[a,r1]|,r1) c= Ball(|[a,r2]|,r2)
proof
  let a be Real;
  let r1,r2 be positive Real;
  assume r1 <= r2;
  then
A1: r2-r1 >= 0 by XREAL_1:48;
  let x be object;
  assume
A2: x in Ball(|[a,r1]|,r1);
  then reconsider x as Element of TOP-REAL 2;
A3: |.x-|[a,r1]|.| < r1 by A2,TOPREAL9:7;
  |[a,r1]|-|[a,r2]| = |[a-a,r1-r2]| by EUCLID:62;
  then |.|[a,r1]|-|[a,r2]|.| = |.r1-r2.| by TOPREAL6:23;
  then |.|[a,r1]|-|[a,r2]|.| = |.r2-r1.| by COMPLEX1:60;
  then |.|[a,r1]|-|[a,r2]|.| = r2-r1 by A1,ABSVALUE:def 1;
  then
A4: |.x-|[a,r1]|.|+|.|[a,r1]|-|[a,r2]|.| < r1+(r2-r1) by A3,XREAL_1:8;
  |.x-|[a,r2]|.| <= |.x-|[a,r1]|.|+|.|[a,r1]|-|[a,r2]|.| by TOPRNS_1:34;
  then |.x-|[a,r2]|.| < r2 by A4,XXREAL_0:2;
  hence thesis by TOPREAL9:7;
end;

theorem Th24:
  for T1,T2 being non empty TopSpace for B1 being
  Neighborhood_System of T1 for B2 being Neighborhood_System of T2 st B1 = B2
  holds the TopStruct of T1 = the TopStruct of T2
proof
  let T1,T2 be non empty TopSpace;
  let B1 be Neighborhood_System of T1;
  let B2 be Neighborhood_System of T2;
A1: dom B1 = the carrier of T1 by PARTFUN1:def 2;
A2: dom B2 = the carrier of T2 by PARTFUN1:def 2;
A3: UniCl Union B2 = the topology of T2 by YELLOW_9:22;
A4: UniCl Union B1 = the topology of T1 by YELLOW_9:22;
  assume B1 = B2;
  hence thesis by A4,A3,A1,A2;
end;

definition
::$N Niemytzki plane
  func Niemytzki-plane -> strict non empty TopSpace means
  :Def3:
  the carrier
of it = y>=0-plane & ex B being Neighborhood_System of it st (for x holds B.(|[
  x,0]|) = {Ball(|[x,r]|,r) \/ {|[x,0]|} where r is Real: r > 0}) &
for x,y st y > 0 holds B.(|[x,y]|) = {Ball(|[x,y]|,r) /\ y>=0-plane where r is
  Real: r > 0};
  existence
  proof
    defpred P[object] means $1 in y=0-line;
    deffunc F1(Element of TOP-REAL 2) = {Ball(|[$1`1,r]|,r) \/ {$1} where r is
    Real: r > 0};
    set X = y>=0-plane;
    deffunc F2(Element of TOP-REAL 2) = {Ball($1,r) /\ X where r is
    Real: r > 0};
    consider B being ManySortedSet of X such that
A1: for a being Element of X st a in X holds (P[a] implies B.a = F1(a)
    ) & (not P[a] implies B.a = F2(a)) from PRE_CIRC:sch 2;
    B is non-empty
    proof
      let z be object;
      assume z in X;
      then reconsider s = z as Element of X;
      per cases;
      suppose
A2:     P[z];
        set r = the positive Element of REAL;
        set a = |[s`1,r]|;
        B.s = F1(s) by A2,A1;
        then Ball(a,r) \/ {s} in B.s;
        hence thesis;
      end;
      suppose
A3:     not P[z];
        set r = the positive Element of REAL;
        B.s = F2(s) by A3,A1;
        then Ball(s,r) /\ X in B.s;
        hence thesis;
      end;
    end;
    then reconsider B as non-empty ManySortedSet of X;
A4: rng B c= bool bool X
    proof
      let w be object;
       reconsider ww=w as set by TARSKI:1;
      assume w in rng B;
      then consider a being object such that
A5:   a in dom B and
A6:   w = B.a by FUNCT_1:def 3;
      reconsider a as Element of X by A5;
      ww c= bool X
      proof
        let z be object;
       reconsider zz=z as set by TARSKI:1;
        assume
A7:     z in ww;
        per cases by A1,A6;
        suppose
          w = F1(a);
          then consider r being Real such that
A8:       z = Ball(|[a`1,r]|,r) \/ {a} and
A9:       r > 0 by A7;
          Ball(|[a`1,r]|,r) c= X by A9,Th20;
          then zz c= X by A8,XBOOLE_1:8;
          hence thesis;
        end;
        suppose
          w = F2(a);
          then
          ex r being Real st z = Ball(a,r) /\ X & r > 0 by A7;
          then zz c= X by XBOOLE_1:17;
          hence thesis;
        end;
      end;
      hence thesis;
    end;
A10: for x,y,U being set st x in U & U in B.y & y in X ex V being set st V
    in B.x & V c= U
    proof
      let x,y,U be set;
      assume
A11:  x in U;
      assume
A12:  U in B.y;
      assume y in X;
      then reconsider y as Element of X;
      per cases;
      suppose
        P[y];
        then B.y = F1(y) by A1;
        then consider r being Real such that
A13:    U = Ball(|[y`1,r]|,r) \/ {y} and
A14:    r > 0 by A12;
A15:    x in Ball(|[y`1,r]|,r) or x = y by A11,A13,ZFMISC_1:136;
        then reconsider z = x as Element of TOP-REAL 2;
        now
          set r2 = r-|.z-|[y`1,r]|.|;
          assume
A16:      x in Ball(|[y`1,r]|,r);
          take V = Ball(z,r2) /\ X;
          |.z-|[y`1,r]|.| < r by A16,TOPREAL9:7;
          then reconsider r1 = r, r2 as positive Real
                by XREAL_1:50;
A17:      r2 > 0;
          Ball(|[y`1,r]|,r) misses y=0-line by A14,Th21;
          then
A18:      not P[x] by A16,XBOOLE_0:3;
          Ball(|[y`1,r]|,r) c= X by A14,Th20;
          then B.z = F2(z) by A16,A18,A1;
          hence V in B.x by A17;
A19:      Ball(|[y`1,r]|,r) c= U by A13,XBOOLE_1:7;
          r1-r2 = |.|[y`1,r]|-z.| by TOPRNS_1:27;
          then
A20:      Ball(z,r2) c= Ball(|[y`1,r]|,r1) by Th22;
          V c= Ball(z,r2) by XBOOLE_1:17;
          then V c= Ball(|[y`1,r]|,r1) by A20;
          hence V c= U by A19;
        end;
        hence thesis by A12,A15;
      end;
      suppose
        not P[y];
        then B.y = F2(y) by A1;
        then consider r being Real such that
A21:    U = Ball(y,r) /\ X and
        r > 0 by A12;
        reconsider z = x as Element of X by A11,A21,XBOOLE_0:def 4;
        set r2 = r-|.z-y.|;
        z in Ball(y,r) by A11,A21,XBOOLE_0:def 4;
        then |.z-y.| < r by TOPREAL9:7;
        then reconsider r1 = r, r2 as positive Real
            by XREAL_1:50;
A22:    z = |[z`1,z`2]| by EUCLID:53;
        per cases;
        suppose
A23:      P[z];
          then z`2 = 0 by A22,Th15;
          then |[z`1,r2/2]|-z = |[z`1-z`1,r2/2-0]| by A22,EUCLID:62;
          then |.|[z`1,r2/2]|-z.| = |.r2/2.| by TOPREAL6:23
            .= r2/2 by ABSVALUE:def 1;
          then |.|[z`1,r2/2]|-y.| <= r2/2+|.z-y.| by TOPRNS_1:34;
          then |.y-|[z`1,r2/2]|.| <= r-r2/2 by TOPRNS_1:27;
          then
A24:      Ball(|[z`1,r2/2]|,r2/2) c= Ball(y,r1) by Th22;
          set V = Ball(|[z`1,r2/2]|,r2/2) \/ {z};
          take V;
          B.z = F1(z) by A23,A1;
          hence V in B.x;
A25:      {z} c= U by A11,ZFMISC_1:31;
          Ball(|[z`1,r2/2]|,r2/2) c= X by Th20;
          then Ball(|[z`1,r2/2]|,r2/2) c= U by A24,A21,XBOOLE_1:19;
          hence thesis by A25,XBOOLE_1:8;
        end;
        suppose
A26:      not P[z];
          take V = Ball(z,r2) /\ X;
          B.z = F2(z) by A26,A1;
          hence V in B.x;
          |.y-z.| = r1-r2 by TOPRNS_1:27;
          hence thesis by A21,Th22,XBOOLE_1:26;
        end;
      end;
    end;
A27: for x,U1,U2 being set st x in X & U1 in B.x & U2 in B.x ex U being
    set st U in B.x & U c= U1 /\ U2
    proof
      let x,U1,U2 be set;
      assume x in X;
      then reconsider z = x as Element of X;
      assume that
A28:  U1 in B.x and
A29:  U2 in B.x;
      per cases;
      suppose
        P[z];
        then
A30:    B.x = F1(z) by A1;
        then consider r1 being Real such that
A31:    U1 = Ball(|[z`1,r1]|,r1) \/ {z} and
A32:    r1 > 0 by A28;
        consider r2 being Real such that
A33:    U2 = Ball(|[z`1,r2]|,r2) \/ {z} and
A34:    r2 > 0 by A29,A30;
        r1 <= r2 or r1 >= r2;
        then consider U being set such that
A35:    r1 <= r2 & U = U1 or r1 >= r2 & U = U2;
A36:    U c= U2 by A31,A32,A33,A35,Th23,XBOOLE_1:9;
        take U;
        thus U in B.x by A28,A29,A35;
        U c= U1 by A31,A33,A34,A35,Th23,XBOOLE_1:9;
        hence thesis by A36,XBOOLE_1:19;
      end;
      suppose
        not P[z];
        then
A37:    B.x = F2(z) by A1;
        then consider r1 being Real such that
A38:    U1 = Ball(z,r1) /\ X and
        r1 > 0 by A28;
        consider r2 being Real such that
A39:    U2 = Ball(z,r2) /\ X and
        r2 > 0 by A29,A37;
        r1 <= r2 or r1 >= r2;
        then consider U being set such that
A40:    r1 <= r2 & U = U1 or r1 >= r2 & U = U2;
A41:    U c= U2 by A38,A39,A40,JORDAN:18,XBOOLE_1:26;
        take U;
        thus U in B.x by A28,A29,A40;
        U c= U1 by A38,A39,A40,JORDAN:18,XBOOLE_1:26;
        hence thesis by A41,XBOOLE_1:19;
      end;
    end;
    for x,U being set st x in X & U in B.x holds x in U
    proof
      let x,U be set;
      assume x in X;
      then reconsider a = x as Element of X;
      assume
A42:  U in B.x;
      per cases by A1;
      suppose
A43:    B.x = F1(a);
A44:    a in {a} by TARSKI:def 1;
        ex r being Real st U = Ball(|[a`1,r]|,r
        ) \/ {a } & r > 0 by A43,A42;
        hence thesis by A44,XBOOLE_0:def 3;
      end;
      suppose
        B.x = F2(a);
        then consider r being Real such that
A45:    U = Ball(a,r) /\ X and
A46:    r > 0 by A42;
        a in Ball(a,r) by A46,Th13;
        hence thesis by A45,XBOOLE_0:def 4;
      end;
    end;
    then consider P being Subset-Family of X such that
    P = Union B and
A47: for T being TopStruct st the carrier of T = X & the topology of
    T = UniCl P holds T is TopSpace & for T9 being non empty TopSpace st T9 = T
    holds B is Neighborhood_System of T9 by A27,A4,A10,TOPGEN_3:3;
    set T = TopStruct(#X, UniCl P#);
    reconsider T as non empty strict TopSpace by A47;
    reconsider B as Neighborhood_System of T by A47;
    take T;
    thus the carrier of T = X;
    take B;
    hereby
      defpred R[Real] means $1 > 0;
      let x;
      deffunc a1(Real) = Ball(|[x,$1]|,$1) \/ {|[x,0]|};
      deffunc a2(Real) = Ball(|[|[x,0]|`1,$1]|,$1) \/ {|[x,0]|};
A48:  |[x,0]| in X;
A49:  for r being Real holds a1(r) = a2(r) by EUCLID:52;

A50:  {a2(r) where r is Real: R[r]}
        c= {a1(r1) where r1 is Real: R[r1]}
      proof let e be object;
       assume e in {a2(r) where r is Real: R[r]};
        then consider r being Real such that
A51:        e = a2(r) & R[r];
        e = a1(r) & R[r] by A49,A51;
       hence e in {a1(r1) where r1 is Real: R[r1]};
      end;
     {a1(r) where r is Real: R[r]}
        c= {a2(r1) where r1 is Real: R[r1]}
      proof let e be object;
       assume e in {a1(r) where r is Real: R[r]};
        then consider r being Real such that
A52:        e = a1(r) & R[r];
        e = a2(r) & R[r] by A49,A52;
       hence e in {a2(r1) where r1 is Real: R[r1]};
      end;
     then
A53:  {a1(r) where r is Real: R[r]}
        = {a2(r) where r is Real: R[r]} by A50;
      P[ |[x,0]| ];
      then B.(|[x,0]|) = F1(|[x,0]|) by A48,A1;
      hence B.(|[x,0]|) = {Ball(|[x,r]|,r) \/ {|[x,0]|}
     where r is Real: r > 0} by A53;
    end;
    let x,y;
    assume
A54: y > 0;
    then
A55: |[x,y]| in X;
    not |[x,y]| in y=0-line by A54,Th15;
    hence thesis by A55,A1;
  end;
  uniqueness
  proof
    let T1,T2 be strict non empty TopSpace such that
A56: the carrier of T1 = y>=0-plane and
A57: ex B being Neighborhood_System of T1 st (for x holds B.(|[x,0]|)
= {Ball(|[x,r]|,r) \/ {|[x,0]|} where r is Real: r > 0}) & for x,y
st y > 0 holds B.(|[x,y]|) = {Ball(|[x,y]|,r) /\ y>=0-plane where r is
 Real: r > 0} and
A58: the carrier of T2 = y>=0-plane and
A59: ex B being Neighborhood_System of T2 st (for x holds B.(|[x,0]|)
  = {Ball(|[x,r]|,r) \/ {|[x,0]|} where r is Real: r > 0}) & for x,y
st y > 0 holds B.(|[x,y]|) = {Ball(|[x,y]|,r) /\ y>=0-plane
  where r is Real: r > 0};
    consider B2 being Neighborhood_System of T2 such that
A60: for x holds B2.(|[x,0]|) = {Ball(|[x,r]|,r) \/ {|[x,0]|} where r
    is Real: r > 0} and
A61: for x,y st y > 0 holds B2.(|[x,y]|) = {Ball(|[x,y]|,r) /\
    y>=0-plane where r is Real: r > 0} by A59;
    consider B1 being Neighborhood_System of T1 such that
A62: for x holds B1.(|[x,0]|) = {Ball(|[x,r]|,r) \/ {|[x,0]|} where r
    is Real: r > 0} and
A63: for x,y st y > 0 holds B1.(|[x,y]|) = {Ball(|[x,y]|,r) /\
    y>=0-plane where r is Real: r > 0} by A57;
    now
      let a be object;
      assume a in y>=0-plane;
      then reconsider z = a as Element of y>=0-plane;
A64:  z = |[z`1,z`2]| by EUCLID:53;
      then z`2 = 0 or z`2 > 0 by Th18;
      then z`2 = 0 & B1.z = {Ball(|[z`1,r]|,r) \/ {|[z`1,0]|} where r is
Real: r > 0} & B2.z = {Ball(|[z`1,r]|,r) \/ {|[z`1,0]|} where r is
Real: r > 0} or z`2 > 0 & B1.z = {Ball(|[z`1,z`2]|,r) /\ y>=0-plane
where r is Real: r > 0} & B2.z = {Ball(|[z`1,z`2]|,r) /\ y>=0-plane
      where r is Real: r > 0} by A62,A63,A60,A61,A64;
      hence B1.a = B2.a;
    end;
    hence thesis by A56,A58,Th24,PBOOLE:3;
  end;
end;

theorem Th25:
  y>=0-plane \ y=0-line is open Subset of Niemytzki-plane
proof
  consider BB being Neighborhood_System of Niemytzki-plane such that
  for x holds BB.(|[x,0]|) = {Ball(|[x,r]|,r) \/ {|[x,0]|} where r is
  Real: r > 0} and
A1: for x,y st y > 0 holds BB.(|[x,y]|) = {Ball(|[x,y]|,r) /\ y>=0-plane
  where r is Real: r > 0} by Def3;
A2: the carrier of Niemytzki-plane = y>=0-plane by Def3;
  then reconsider A = y>=0-plane \ y=0-line as Subset of Niemytzki-plane by
XBOOLE_1:36;
  now
    let a be Point of Niemytzki-plane;
    assume
A3: a in A;
    then a in y>=0-plane by XBOOLE_0:def 5;
    then consider x,y such that
A4: a = |[x,y]| and
A5: y >= 0;
    set B = Ball(|[x,y]|,y)/\y>=0-plane;
    reconsider B as Subset of Niemytzki-plane by A2,XBOOLE_1:17;
    not a in y=0-line by A3,XBOOLE_0:def 5;
    then
A6: y <> 0 by A4;
    then B in {Ball(|[x,y]|,r) /\ y>=0-plane where r is Real: r >
    0} by A5;
    then
A7: B in BB.a by A1,A4,A5,A6;
    take B;
    dom BB = the carrier of Niemytzki-plane by PARTFUN1:def 2;
    hence B in Union BB by A7,CARD_5:2;
    thus a in B by A7,YELLOW_8:12;
    Ball(|[x,y]|,y) c= y>=0-plane by A5,A6,Th20;
    then B = Ball(|[x,y]|,y) by XBOOLE_1:28;
    then B misses y=0-line by A5,A6,Th21;
    hence B c= A by A2,XBOOLE_1:86;
  end;
  hence thesis by YELLOW_9:31;
end;

Lm1: the carrier of Niemytzki-plane = y>=0-plane by Def3;

theorem Th26:
  y=0-line is closed Subset of Niemytzki-plane
proof
  reconsider B = y=0-line as Subset of Niemytzki-plane by Def3,Th19;
  reconsider A = y>=0-plane \ y=0-line as open Subset of Niemytzki-plane by
Th25;
  B` = A by Def3;
  then A` = y=0-line;
  hence thesis;
end;

theorem Th27:
  for x being Real, r being positive Real holds
  Ball(|[x,r]|,r) \/ {|[x,0]|} is open Subset of Niemytzki-plane
proof
  let x be Real;
  let r be positive Real;
  the carrier of Niemytzki-plane = y>=0-plane by Def3;
  then reconsider a = |[x,0]| as Point of Niemytzki-plane by Th18;
  consider BB being Neighborhood_System of Niemytzki-plane such that
A1: for x holds BB.(|[x,0]|) = {Ball(|[x,q]|,q) \/ {|[x,0]|} where q is
  Real: q > 0} and
  for x,y st y > 0 holds BB.(|[x,y]|) = {Ball(|[x,y]|,q) /\ y>=0-plane
  where q is Real: q > 0} by Def3;
  BB.(|[x,0]|) = {Ball(|[x,q]|,q) \/ {|[x,0]|} where q is Real:
  q > 0} by A1;
  then Ball(|[x,r]|,r) \/ {|[x,0]|} in BB.a;
  hence thesis by YELLOW_8:12;
end;

theorem Th28:
  for x being Real for y,r being positive Real
  holds Ball(|[x,y]|,r) /\ y>=0-plane is open Subset of Niemytzki-plane
proof
  let x be Real;
  let y,r be positive Real;
  the carrier of Niemytzki-plane = y>=0-plane by Def3;
  then reconsider a = |[x,y]| as Point of Niemytzki-plane by Th18;
  consider BB being Neighborhood_System of Niemytzki-plane such that
  for x holds BB.(|[x,0]|) = {Ball(|[x,q]|,q) \/ {|[x,0]|} where q is
  Real: q > 0} and
A1: for x,y st y > 0 holds BB.(|[x,y]|) = {Ball(|[x,y]|,q) /\ y>=0-plane
  where q is Real: q > 0} by Def3;
  BB.(|[x,y]|) = {Ball(|[x,y]|,q) /\ y>=0-plane where q is Real
  : q > 0} by A1;
  then Ball(|[x,y]|,r) /\ y>=0-plane in BB.a;
  hence thesis by YELLOW_8:12;
end;

theorem Th29:
  for x,y being Real for r being positive Real st
  r <= y holds Ball(|[x,y]|,r) is open Subset of Niemytzki-plane
proof
  let x,y be Real;
  let r be positive Real;
  assume
A1: r <= y;
A2: Ball(|[x,y]|,r) c= y>=0-plane
  proof
    let a be object;
    assume
A3: a in Ball(|[x,y]|,r);
    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 thesis by A4,A1,A5,XXREAL_0:2;
  end;
  Ball(|[x,y]|,r) /\ y>=0-plane is open Subset of Niemytzki-plane by A1,Th28;
  hence thesis by A2,XBOOLE_1:28;
end;

theorem Th30:
  for p being Point of Niemytzki-plane for r being positive Real
 ex a being Point of TOP-REAL 2, U being open Subset of Niemytzki-plane
st p in U & a in U & for b being Point of TOP-REAL 2 st b in U holds |.b-a.| <
  r
proof
  let p be Point of Niemytzki-plane;
  let r be positive Real;
  consider BB being Neighborhood_System of Niemytzki-plane such that
A1: for x holds BB.(|[x,0]|) = {Ball(|[x,q]|,q) \/ {|[x,0]|} where q is
    Real: q > 0} and
A2: for x,y st y > 0 holds BB.(|[x,y]|) = {Ball(|[x,y]|,q) /\ y>=0-plane
  where q is Real: q > 0} by Def3;
A3: the carrier of Niemytzki-plane = y>=0-plane by Def3;
  p in the carrier of Niemytzki-plane;
  then reconsider p9 = p as Point of TOP-REAL 2 by A3;
A4: p = |[p9`1,p9`2]| by EUCLID:53;
  per cases by A3,A4,Th18;
  suppose
A5: p9`2 = 0;
    then
    BB.p = {Ball(|[p9`1,q]|,q) \/ {|[p9`1,0]|} where q is Real:
    q > 0} by A1,A4;
    then
A6: Ball(|[p9`1,r/2]|,r/2) \/ {|[p9`1,0]|} in BB.p;
    BB.p c= the topology of Niemytzki-plane by TOPS_2:64;
    then reconsider U = Ball(|[p9`1,r/2]|,r/2) \/ {p} as open Subset of
    Niemytzki-plane by A6,A4,A5,PRE_TOPC:def 2;
    take a = |[p9`1,r/2]|, U;
    thus p in U by ZFMISC_1:136;
A7: r/2 < r/2+r/2 by XREAL_1:29;
    a in Ball(a,r/2) by Th13;
    hence a in U by XBOOLE_0:def 3;
    let b be Point of TOP-REAL 2;
    assume b in U;
    then
A8: b in Ball(a,r/2) or b = p by ZFMISC_1:136;
    p9-a = |[p9`1-p9`1,0-r/2]| by A4,A5,EUCLID:62;
    then |.p9-a.| = |.0-r/2.| by TOPREAL6:23
      .= |.r/2-0 .| by COMPLEX1:60
      .= r/2 by ABSVALUE:def 1;
    then |.b-a.| <= r/2 by A8,TOPREAL9:7;
    hence thesis by A7,XXREAL_0:2;
  end;
  suppose
A9: p9`2 > 0;
    then BB.p = {Ball(|[p9`1,p9`2]|,q) /\ y>=0-plane
   where q is Real: q > 0} by A2,A4;
    then
A10: Ball(p9,r/2) /\ y>=0-plane in BB.p by A4;
    BB.p c= the topology of Niemytzki-plane by TOPS_2:64;
    then reconsider U = Ball(p9,r/2) /\ y>=0-plane as open Subset of
    Niemytzki-plane by A10,PRE_TOPC:def 2;
    take a = p9, U;
A11: p in Ball(a,r/2) by Th13;
    p in y>=0-plane by A4,A9;
    hence p in U & a in U by A11,XBOOLE_0:def 4;
    let b be Point of TOP-REAL 2;
    assume b in U;
    then b in Ball(a,r/2) by XBOOLE_0:def 4;
    then
A12: |.b-a.| <= r/2 by TOPREAL9:7;
    r/2 < r/2+r/2 by XREAL_1:29;
    hence thesis by A12,XXREAL_0:2;
  end;
end;

theorem Th31:
  for x,y being Real for r being positive Real ex
  w,v being Rational st |[w,v]| in Ball(|[x,y]|,r) & |[w,v]| <> |[x,y]|
proof
  let x,y be Real;
  let r be positive Real;
  x < x+r/2 by XREAL_1:39;
  then consider w being Rational such that
A1: x < w and
A2: w < x+r/2 by RAT_1:7;
A3: w-x > 0 by A1,XREAL_1:50;
  y < y+r/2 by XREAL_1:39;
  then consider v being Rational such that
A4: y < v and
A5: v < y+r/2 by RAT_1:7;
A6: v-y > 0 by A4,XREAL_1:50;
  |[w,v]|-|[x,v]| = |[w-x,v-v]| by EUCLID:62;
  then |.|[w,v]|-|[x,v]|.| = |.w-x.| by TOPREAL6:23;
  then |.|[w,v]|-|[x,v]|.| = w-x by A3,ABSVALUE:def 1;
  then
A7: |.|[w,v]|-|[x,v]|.| < x+r/2-x by A2,XREAL_1:9;
  take w,v;
A8: |[x,v]|-|[x,y]| = |[x-x,v-y]| by EUCLID:62;
A9: |.|[w,v]|-|[x,y]|.| <= |.|[w,v]|-|[x,v]|.|+|.|[x,v]|-|[x,y]|.| by
TOPRNS_1:34;
  |.|[x,v]|-|[x,y]|.| = |.v-y.| by A8,TOPREAL6:23;
  then |.|[x,v]|-|[x,y]|.| = v-y by A6,ABSVALUE:def 1;
  then |.|[x,v]|-|[x,y]|.| <= y+r/2-y by A5,XREAL_1:9;
  then |.|[w,v]|-|[x,v]|.|+|.|[x,v]|-|[x,y]|.| < x+r/2-x+(y+r/2-y) by A7,
XREAL_1:8;
  then |.|[w,v]|-|[x,y]|.| < r by A9,XXREAL_0:2;
  hence |[w,v]| in Ball(|[x,y]|,r) by TOPREAL9:7;
  thus thesis by A4,SPPOL_2:1;
end;

theorem Th32:
  for A being Subset of Niemytzki-plane st A = (y>=0-plane \
  y=0-line) /\ product <*RAT,RAT*> for x being set holds Cl (A \ {x}) = [#]
  Niemytzki-plane
proof
  let A be Subset of Niemytzki-plane;
  assume
A1: A = (y>=0-plane \ y=0-line) /\ product <*RAT,RAT*>;
  let s be set;
  thus Cl (A\{s}) c= [#] Niemytzki-plane;
  let x be object;
  assume x in [#] Niemytzki-plane;
  then reconsider a = x as Element of Niemytzki-plane;
  reconsider b = a as Element of y>=0-plane by Def3;
  consider BB being Neighborhood_System of Niemytzki-plane such that
A2: for x holds BB.(|[x,0]|) = {Ball(|[x,q]|,q) \/ {|[x,0]|} where q is
  Real: q > 0} and
A3: for x,y st y > 0 holds BB.(|[x,y]|) = {Ball(|[x,y]|,q) /\ y>=0-plane
  where q is Real: q > 0} by Def3;
A4: a = |[b`1,b`2]| by EUCLID:53;
  for U being set st U in BB.a holds U meets A\{s}
  proof
    let U be set;
    assume
A5: U in BB.a;
    per cases by A4,Th18;
    suppose
A6:   b`2 = 0;
      then
      BB.a = {Ball(|[b`1,q]|,q) \/ {|[b`1,0]|} where q is Real
      : q > 0} by A2,A4;
      then consider q being Real such that
A7:   U = Ball(|[b`1,q]|,q) \/ {a} and
A8:   q > 0 by A4,A5,A6;
      reconsider q as positive Real by A8;
      consider w1,v1 being Rational such that
A9:   |[w1,v1]| in Ball(|[b`1,q]|,q) and
A10:  |[w1,v1]| <> |[b`1,q]| by Th31;
A11:  |[w1,v1]| in U by A7,A9,XBOOLE_0:def 3;
      set q2 = |.|[w1,v1]|-|[b`1,q]|.|;
      |[w1,v1]|-|[b`1,q]| <> 0.TOP-REAL 2 by A10,RLVECT_1:21;
      then q2 <> 0 by EUCLID_2:42;
      then reconsider q2 as positive Real;
A12:  q2 < q by A9,TOPREAL9:7;
      consider w2,v2 being Rational such that
A13:  |[w2,v2]| in Ball(|[b`1,q]|,q2) and
      |[w2,v2]| <> |[b`1,q]| by Th31;
      |.|[w2,v2]|-|[b`1,q]|.| < q2 by A13,TOPREAL9:7;
      then |.|[w2,v2]|-|[b`1,q]|.| < q by A12,XXREAL_0:2;
      then
A14:  |[w2,v2]| in Ball(|[b`1,q]|,q) by TOPREAL9:7;
      then
A15:  |[w2,v2]| in U by A7,XBOOLE_0:def 3;
A16:  Ball(|[b`1,q]|,q) misses y=0-line by Th21;
      Ball(|[b`1,q]|,q) c= y>=0-plane by Th20;
      then
A17:  Ball(|[b`1,q]|,q) c= y>=0-plane \ y=0-line by A16,XBOOLE_1:86;
A18:  v1 in RAT by RAT_1:def 2;
      w1 in RAT by RAT_1:def 2;
      then |[w1,v1]| in product <*RAT, RAT*> by A18,FINSEQ_3:124;
      then
A19:  |[w1,v1]| in A by A17,A9,A1,XBOOLE_0:def 4;
A20:  s = |[w1,v1]| or s <> |[w1,v1]|;
A21:  v2 in RAT by RAT_1:def 2;
      w2 in RAT by RAT_1:def 2;
      then |[w2,v2]| in product <*RAT,RAT*> by A21,FINSEQ_3:124;
      then
A22:  |[w2,v2]| in A by A17,A14,A1,XBOOLE_0:def 4;
      |[w2,v2]| <> |[w1,v1]| by A13,TOPREAL9:7;
      then |[w1,v1]| in A\{s} or |[w2,v2]| in A\{s} by A20,A19,A22,ZFMISC_1:56;
      hence thesis by A11,A15,XBOOLE_0:3;
    end;
    suppose
A23:  b`2 > 0;
      then BB.a = {Ball(|[b`1,b`2]|,q) /\ y>=0-plane
     where q is Real: q > 0} by A3,A4;
      then consider q being Real such that
A24:  U = Ball(b,q) /\ y>=0-plane and
A25:  q > 0 by A4,A5;
      reconsider q, b2 = b`2 as positive Real by A23,A25;
      reconsider q1 = min(q,b2) as positive Real by XXREAL_0:def 9;
      consider w1,v1 being Rational such that
A26:  |[w1,v1]| in Ball(b,q1) and
A27:  |[w1,v1]| <> b by A4,Th31;
A28:  v1 in RAT by RAT_1:def 2;
      set q2 = |.|[w1,v1]|-b.|;
      |[w1,v1]|-b <> 0.TOP-REAL 2 by A27,RLVECT_1:21;
      then q2 <> 0 by EUCLID_2:42;
      then reconsider q2 as positive Real;
A29:  q2 < q1 by A26,TOPREAL9:7;
A30:  q1 <= b`2 by XXREAL_0:17;
      then
A31:  Ball(b,q1) c= y>=0-plane by A4,Th20;
      Ball(b,q1) misses y=0-line by A30,A4,Th21;
      then
A32:  Ball(b,q1) c= y>=0-plane \ y=0-line by A31,XBOOLE_1:86;
      w1 in RAT by RAT_1:def 2;
      then |[w1,v1]| in product <*RAT, RAT*> by A28,FINSEQ_3:124;
      then
A33:  |[w1,v1]| in A by A32,A26,A1,XBOOLE_0:def 4;
A34:  s = |[w1,v1]| or s <> |[w1,v1]|;
      consider w2,v2 being Rational such that
A35:  |[w2,v2]| in Ball(b,q2) and
      |[w2,v2]| <> b by A4,Th31;
A36:  |[w2,v2]| <> |[w1,v1]| by A35,TOPREAL9:7;
      |.|[w2,v2]|-b.| < q2 by A35,TOPREAL9:7;
      then
A37:  |.|[w2,v2]|-b.| < q1 by A29,XXREAL_0:2;
      then
A38:  |[w2,v2]| in Ball(b,q1) by TOPREAL9:7;
A39:  q1 <= q by XXREAL_0:17;
      then |.|[w2,v2]|-b.| < q by A37,XXREAL_0:2;
      then |[w2,v2]| in Ball(b,q) by TOPREAL9:7;
      then
A40:  |[w2,v2]| in U by A24,A38,A31,XBOOLE_0:def 4;
A41:  v2 in RAT by RAT_1:def 2;
      w2 in RAT by RAT_1:def 2;
      then |[w2,v2]| in product <*RAT,RAT*> by A41,FINSEQ_3:124;
      then |[w2,v2]| in A by A32,A38,A1,XBOOLE_0:def 4;
      then
A42:  |[w1,v1]| in A\{s} or |[w2,v2]| in A\{s} by A34,A36,A33,ZFMISC_1:56;
      q2 < q by A39,A29,XXREAL_0:2;
      then |[w1,v1]| in Ball(b,q) by TOPREAL9:7;
      then |[w1,v1]| in U by A24,A26,A31,XBOOLE_0:def 4;
      hence thesis by A42,A40,XBOOLE_0:3;
    end;
  end;
  hence thesis by TOPGEN_2:10;
end;

theorem Th33:
  for A being Subset of Niemytzki-plane st A = y>=0-plane \
  y=0-line for x being set holds Cl (A \ {x}) = [#] Niemytzki-plane
proof
  let A be Subset of Niemytzki-plane;
  assume
A1: A = y>=0-plane \ y=0-line;
  let s be set;
  reconsider B = A /\ product <*RAT,RAT*> as Subset of Niemytzki-plane;
  thus Cl (A\{s}) c= [#] Niemytzki-plane;
  B\{s} c= A\{s} by XBOOLE_1:17,33;
  then Cl (B\{s}) c= Cl (A\{s}) by PRE_TOPC:19;
  hence thesis by A1,Th32;
end;

theorem Th34:
  for A being Subset of Niemytzki-plane st A = y>=0-plane \
  y=0-line holds Cl A = [#] Niemytzki-plane
proof
  let A be Subset of Niemytzki-plane;
  A\{A} = A
  proof
    thus A\{A} c= A by XBOOLE_1:36;
    let x be object;
    not A in A;
    hence thesis by ZFMISC_1:56;
  end;
  hence thesis by Th33;
end;

theorem Th35:
  for A being Subset of Niemytzki-plane st A = y=0-line holds Cl A
  = A & Int A = {}
proof
  let A be Subset of Niemytzki-plane;
  assume
A1: A = y=0-line;
  then
A2: A` = y>=0-plane \ y=0-line by Def3;
  thus Cl A = A by A1,Th26,PRE_TOPC:22;
  thus Int A = (Cl A`)` by TOPS_1:def 1
    .= ([#] Niemytzki-plane)` by A2,Th34
    .= {} by XBOOLE_1:37;
end;

theorem Th36:
  (y>=0-plane \ y=0-line) /\ product <*RAT,RAT*> is dense Subset
  of Niemytzki-plane
proof
  (y>=0-plane \ y=0-line) /\ product <*RAT,RAT*> c= y>=0-plane \ y=0-line
  by XBOOLE_1:17;
  then reconsider
  A = (y>=0-plane \ y=0-line) /\ product <*RAT,RAT*> as Subset of
  Niemytzki-plane by Th25,XBOOLE_1:1;
  A\{A} = A
  proof
    thus A\{A} c= A by XBOOLE_1:36;
    let x be object;
    not A in A;
    hence thesis by ZFMISC_1:56;
  end;
  then Cl A = [#] Niemytzki-plane by Th32;
  hence thesis by TOPS_1:def 3;
end;

theorem
  (y>=0-plane \ y=0-line) /\ product <*RAT,RAT*> is dense-in-itself
  Subset of Niemytzki-plane
proof
  (y>=0-plane \ y=0-line) /\ product <*RAT,RAT*> c= y>=0-plane \ y=0-line
  by XBOOLE_1:17;
  then reconsider
  A = (y>=0-plane \ y=0-line) /\ product <*RAT,RAT*> as Subset of
  Niemytzki-plane by Th25,XBOOLE_1:1;
  A is dense-in-itself
  proof
    let a be object;
    assume a in A;
    then reconsider x = a as Point of Niemytzki-plane;
    Cl (A\{x}) = the carrier of Niemytzki-plane by Th32;
    then x is_an_accumulation_point_of A;
    hence thesis by TOPGEN_1:def 3;
  end;
  hence thesis;
end;

theorem
  y>=0-plane \ y=0-line is dense Subset of Niemytzki-plane
proof
  reconsider A = y>=0-plane \ y=0-line as open Subset of Niemytzki-plane by
Th25;
  Cl A = [#] Niemytzki-plane by Th34;
  hence thesis by TOPS_1:def 3;
end;

theorem
  y>=0-plane \ y=0-line is dense-in-itself Subset of Niemytzki-plane
proof
  the carrier of Niemytzki-plane = y>=0-plane by Def3;
  then reconsider A = y>=0-plane \ y=0-line as Subset of Niemytzki-plane by
XBOOLE_1:36;
  A is dense-in-itself
  proof
    let a be object;
    assume a in A;
    then reconsider x = a as Point of Niemytzki-plane;
    Cl (A\{x}) = the carrier of Niemytzki-plane by Th33;
    then x is_an_accumulation_point_of A;
    hence thesis by TOPGEN_1:def 3;
  end;
  hence thesis;
end;

theorem
  y=0-line is nowhere_dense Subset of Niemytzki-plane
proof
  reconsider A = y=0-line as Subset of Niemytzki-plane by Def3,Th19;
  Int Cl A = Int A by Th26,PRE_TOPC:22
    .= {} by Th35;
  hence thesis by TOPS_3:def 3;
end;

theorem Th41:
  for A being Subset of Niemytzki-plane st A = y=0-line holds Der A is empty
proof
  consider BB being Neighborhood_System of Niemytzki-plane such that
A1: for x holds BB.(|[x,0]|) = {Ball(|[x,r]|,r) \/ {|[x,0]|} where r is
  Real: r > 0} and
  for x,y st y > 0 holds BB.(|[x,y]|) = {Ball(|[x,y]|,r) /\ y>=0-plane
  where r is Real: r > 0} by Def3;
  let A be Subset of Niemytzki-plane;
  assume that
A2: A = y=0-line and
A3: Der A is not empty;
  set a = the Element of Der A;
  a in Der A by A3;
  then reconsider a as Point of Niemytzki-plane;
A4: a in Der A by A3;
  a is_an_accumulation_point_of A by A3,TOPGEN_1:def 3;
  then
A5: a in Cl (A \ {a});
  the carrier of Niemytzki-plane = y>=0-plane by Def3;
  then a in y>=0-plane;
  then reconsider b = a as Point of TOP-REAL 2;
A6: a = |[b`1,b`2]| by EUCLID:53;
A7: Der A c= Cl A by TOPGEN_1:28;
  Cl A = A by A2,Th35;
  then
A8: b`2 = 0 by A4,A7,A2,A6,Th15;
  then
  BB.a = {Ball(|[b`1,r]|,r) \/ {|[b`1,0]|} where r is Real:
    r > 0 } by A1,A6;
  then Ball(|[b`1,1]|,1) \/ {b} in BB.a by A6,A8;
  then Ball(|[b`1,1]|,1) \/ {b} meets A \ {a} by A5,TOPGEN_2:9;
  then consider z being object such that
A9: z in Ball(|[b`1,1]|,1) \/ {b} and
A10: z in A \ {a} by XBOOLE_0:3;
A11: z in A by A10,ZFMISC_1:56;
  z <> a by A10,ZFMISC_1:56;
  then
A12: z in Ball(|[b`1,1]|,1) by A9,ZFMISC_1:136;
  reconsider z as Point of TOP-REAL 2 by A9;
A13: z = |[z`1,z`2]| by EUCLID:53;
  then z`2 = 0 by A2,A11,Th15;
  then
A14: z-|[b`1,1]| = |[z`1-b`1,0-1]| by A13,EUCLID:62;
A15: |[z`1-b`1,0-1]|`2 = 0-1 by EUCLID:52;
  |[z`1-b`1,0-1]|`1 = z`1-b`1 by EUCLID:52;
  then |.z-|[b`1,1]|.| = sqrt((z`1-b`1)^2+(-1)^2) by A14,A15,JGRAPH_1:30
    .= sqrt((z`1-b`1)^2+1^2);
  then
A16: |.z-|[b`1,1]|.| >= |.1.| by COMPLEX1:79;
  |.z-|[b`1,1]|.| < 1 by A12,TOPREAL9:7;
  then |.1.| < 1 by A16,XXREAL_0:2;
  hence contradiction by ABSVALUE:4;
end;

theorem Th42:
  for A being Subset of y=0-line holds A is closed Subset of Niemytzki-plane
proof
  reconsider B = y=0-line as closed Subset of Niemytzki-plane by Th26;
  let A be Subset of y=0-line;
  A c= B;
  then reconsider A as Subset of Niemytzki-plane by XBOOLE_1:1;
  Der A c= Der B by TOPGEN_1:30;
  then Der A c= {} by Th41;
  then Der A = {};
  then Cl A = A \/ {} by TOPGEN_1:29;
  hence thesis;
end;

theorem Th43:
  RAT is dense Subset of Sorgenfrey-line
proof
  reconsider A = RAT as Subset of Sorgenfrey-line by NUMBERS:12,TOPGEN_3:def 2;
  consider B being Subset-Family of REAL such that
A1: the topology of Sorgenfrey-line = UniCl B and
A2: B = {[.x,q.[ where x,q is Real: x < q & q is rational}
          by TOPGEN_3:def 2;
  the carrier of Sorgenfrey-line = REAL by TOPGEN_3:def 2;
  then
A3: B is Basis of Sorgenfrey-line by A1,YELLOW_9:22;
  A is dense
  proof
    thus Cl A c= the carrier of Sorgenfrey-line;
    let x be object;
    assume x in the carrier of Sorgenfrey-line;
    then reconsider x as Point of Sorgenfrey-line;
    now
      let C be Subset of Sorgenfrey-line;
      assume C in B;
      then consider y,q being Real such that
A4:   C = [.y,q.[ and
A5:   y < q and
      q is rational by A2;
      assume x in C;
      consider r being Rational such that
A6:   y < r and
A7:   r < q by A5,RAT_1:7;
A8:   r in A by RAT_1:def 2;
      r in C by A4,A6,A7,XXREAL_1:3;
      hence A meets C by A8,XBOOLE_0:3;
    end;
    hence thesis by A3,YELLOW_9:37;
  end;
  hence thesis;
end;

theorem
  Sorgenfrey-line is separable
by Th43,TOPGEN_1:def 12,TOPGEN_3:17;

theorem
  Niemytzki-plane is separable
proof
  reconsider A = (y>=0-plane \ y=0-line) /\ product <*RAT,RAT*> as dense
  Subset of Niemytzki-plane by Th36;
A1: card A c= card product <*RAT, RAT*> by CARD_1:11,XBOOLE_1:17;
  density Niemytzki-plane c= card A by TOPGEN_1:def 12;
  then density Niemytzki-plane c= card product <*RAT,RAT*> by A1;
  hence density Niemytzki-plane c= omega by Th8,CARD_4:6,TOPGEN_3:17;
end;

theorem
  Niemytzki-plane is T_1
proof
  set T = Niemytzki-plane;
  let p,q be Point of T such that
A1: p <> q;
A2: q in the carrier of T;
A3: the carrier of T = y>=0-plane by Def3;
  p in the carrier of T;
  then reconsider p9 = p, q9 = q as Point of TOP-REAL 2 by A2,A3;
  p9-q9 <> 0.TOP-REAL 2 by A1,RLVECT_1:21;
  then |.p9-q9.| <> 0 by EUCLID_2:42;
  then reconsider r = |.p9-q9.| as positive Real;
  consider ap being Point of TOP-REAL 2, Up being open Subset of T such that
A4: p in Up and
  ap in Up and
A5: for b being Point of TOP-REAL 2 st b in Up holds |.b-ap.| < r/2 by Th30;
  consider aq being Point of TOP-REAL 2, Uq being open Subset of T such that
A6: q in Uq and
  aq in Uq and
A7: for b being Point of TOP-REAL 2 st b in Uq holds |.b-aq.| < r/2 by Th30;
  take Up,Uq;
  thus Up is open & Uq is open & p in Up by A4;
  thus not q in Up
  proof
    assume q in Up;
    then
A8: |.q9-ap.| < r/2 by A5;
    |.q9-ap.| = |.ap-q9.| by TOPRNS_1:27;
    then |.p9-ap.|+|.ap-q9.| < r/2+r/2 by A8,A4,A5,XREAL_1:8;
    hence contradiction by TOPRNS_1:34;
  end;
  thus q in Uq by A6;
  assume
A9: p in Uq;
A10: |.q9-aq.| = |.aq-q9.| by TOPRNS_1:27;
  |.q9-aq.| < r/2 by A6,A7;
  then |.p9-aq.|+|.aq-q9.| < r/2+r/2 by A10,A9,A7,XREAL_1:8;
  hence contradiction by TOPRNS_1:34;
end;

theorem
  Niemytzki-plane is not normal
proof
  reconsider C = (y>=0-plane \ y=0-line) /\ product <*RAT,RAT*> as dense
  Subset of Niemytzki-plane by Th36;
  set T = Niemytzki-plane;
  defpred P[object,object] means
    ex D1 being set, U,V being open Subset of T st D1 = $1 &  $2 = U /\ C & D1
       c= U & y=0-line \ D1 c= V & U misses V;
A1: exp(2, omega) in exp(2, exp(2, omega)) by CARD_5:14;
  card C c= card product <*RAT,RAT*> by CARD_1:11,XBOOLE_1:17;
  then card C c= omega by Th8,CARD_4:6,TOPGEN_3:17;
  then
A2: exp(2, card C) c= exp(2, omega) by CARD_2:93;
  assume
A3: for W, V being Subset of T st W <> {} & V <> {} & W is closed & V is
closed & W misses V ex P, Q being Subset of T st P is open & Q is open & W c= P
  & V c= Q & P misses Q;
A4: for a being object st a in bool y=0-line ex b being object st P[a,b]
  proof
    let a be object;
    assume a in bool y=0-line;
    then reconsider aa = a as Subset of y=0-line;
    reconsider a9 = y=0-line \ aa as Subset of y=0-line by
XBOOLE_1:36;
    reconsider A = aa, B = a9 as closed Subset of T by Th42;
    per cases;
    suppose
A5:   a = {};
      take {};
      take {},{}T,[#]T;
      thus thesis by A5,Def3,Th19;
    end;
    suppose
A6:   a = y=0-line;
      take ([#]T)/\ C;
      take aa,[#]T,{}T;
      thus aa = a;
      thus thesis by A6,Def3,Th19,XBOOLE_1:37;
    end;
    suppose
A7:   a <> {} & a <> y=0-line;
      aa`` = a9`;
      then
A8:   B <> {}y=0-line by A7;
      A misses B by XBOOLE_1:79;
      then consider P, Q being Subset of T such that
A9:   P is open and
A10:  Q is open and
A11:  A c= P and
A12:  B c= Q and
A13:  P misses Q by A8,A3,A7;
      take P /\ C;
      thus thesis by A9,A10,A11,A12,A13;
    end;
  end;
  consider G being Function such that
A14: dom G = bool y=0-line and
A15: for a being object st a in bool y=0-line holds P[a,G.a] from CLASSES1:
  sch 1(A4);
  G is one-to-one
  proof
    let x,y be object;
    assume that
A16: x in dom G and
A17: y in dom G;
    reconsider A = x, B = y as Subset of y=0-line by A16,A17,A14;
    assume that
A18: G.x = G.y and
A19: x <> y;
    consider z being object such that
A20: not (z in A iff z in B) by A19,TARSKI:2;
A21: z in A\B or z in B\A by A20,XBOOLE_0:def 5;
    consider D1 being set,UB,VB being open Subset of T such that
A22:  D1 = B and
A23: G.B = UB /\ C and
A24: D1 c= UB and
A25: y=0-line \ D1 c= VB and
A26: UB misses VB by A15;
    consider D1 being set,UA,VA being open Subset of T such that
A27:  D1 = A and
A28: G.A = UA /\ C and
A29: D1 c= UA and
A30: y=0-line \ D1 c= VA and
A31: UA misses VA by A15;
    B\A = B/\A` by SUBSET_1:13;
    then
A32: B\A c= UB /\ VA by A30,A24,XBOOLE_1:27,A22,A27;
    A\B = A/\B` by SUBSET_1:13;
    then A\B c= UA /\ VB by A29,A25,XBOOLE_1:27,A22,A27;
    then C meets UA /\ VB or C meets UB /\ VA by A32,A21,TOPS_1:45;
    then (ex z being object st z in C & z in UA /\ VB)
or ex z being object st z in
    C & z in UB /\ VA by XBOOLE_0:3;
    then consider z being set such that
A33: z in C and
A34: z in UA /\ VB or z in UB /\ VA;
    z in UA & z in VB or z in UB & z in VA by A34,XBOOLE_0:def 4;
    then z in UA & not z in UB or z in UB & not z in UA by A31,A26,XBOOLE_0:3;
    then z in G.A & not z in G.B or z in G.B & not z in G.A by A28,A23,A33,
XBOOLE_0:def 4;
    hence thesis by A18;
  end;
  then
A35: card dom G c= card rng G by CARD_1:10;
  rng G c= bool C
  proof
    let a be object;
       reconsider aa=a as set by TARSKI:1;
    assume a in rng G;
    then consider b being object such that
A36: b in dom G and
A37: a = G.b by FUNCT_1:def 3;
    P[b,aa] by A14,A15,A36,A37;
    then aa c= C by XBOOLE_1:17;
    hence thesis;
  end;
  then card rng G c= card bool C by CARD_1:11;
  then card bool y=0-line c= card bool C by A35,A14;
  then
A38: exp(2, continuum) c= card bool C by Th16,CARD_2:31;
  card bool C = exp(2, card C) by CARD_2:31;
  then exp(2, continuum) c= exp(2, omega) by A38,A2;
  then exp(2, omega) in exp(2, omega) by A1,TOPGEN_3:29;
  hence contradiction;
end;

begin :: Tychonoff spaces

definition
  let T be TopSpace;
  attr T is Tychonoff means

  for A being closed Subset of T, a being
Point of T st a in A` ex f being continuous Function of T, I[01] st f.a = 0 & f
  .:A c= {1};
end;

registration
  cluster Tychonoff -> regular for TopSpace;
  coherence
  proof
    reconsider z = 0, j = 1, half = 1/2 as Element of I[01] by BORSUK_1:40
,XXREAL_1:1;
    let T be TopSpace;
    assume that
A1: for A being closed Subset of T, a being Point of T st a in A` ex f
    being continuous Function of T, I[01] st f.a = 0 & f.:A c= {1};
    reconsider A = [.z,half.[, B = ].half,j.] as Subset of I[01] by BORSUK_1:40
,XXREAL_1:35,36;
    reconsider A,B as open Subset of I[01] by TOPALG_1:4,5;
    let p be Point of T, P be Subset of T;
    assume that
A2: P is closed and
A3: p in P`;
    consider f being continuous Function of T, I[01] such that
A4: f.p = 0 and
A5: f.:P c= {1} by A2,A3,A1;
    take W = f"A, V = f"B;
    [#]I[01] <> {};
    hence W is open & V is open by TOPS_2:43;
    0 in A by XXREAL_1:3;
    hence p in W by A3,A4,FUNCT_2:38;
A6: dom f = the carrier of T by FUNCT_2:def 1;
    1 in B by XXREAL_1:2;
    then {1} c= B by ZFMISC_1:31;
    then f.:P c= B by A5;
    hence P c= V by A6,FUNCT_1:93;
    assume W meets V;
    then consider x being object such that
A7: x in W and
A8: x in V by XBOOLE_0:3;
A9: f.x in A by A7,FUNCT_1:def 7;
    then reconsider fx = f.x as Element of I[01];
A10: fx < half by A9,XXREAL_1:3;
    f.x in B by A8,FUNCT_1:def 7;
    hence thesis by A10,XXREAL_1:2;
  end;
  cluster T_4 -> Tychonoff for non empty TopSpace;
  coherence
  proof
    the carrier of Closed-Interval-TSpace(-1,1) = [.-1,1.] by TOPMETR:18;
    then reconsider j = 1, k = -1 as Point of Closed-Interval-TSpace(-1,1) by
XXREAL_1:1;
    reconsider z = 0, o = 1 as Point of I[01] by BORSUK_1:40,XXREAL_1:1;
    let T be non empty TopSpace;
    assume
A11: T is T_4;
    let A be closed Subset of T, a be Point of T;
    per cases;
    suppose
A12:  A is empty;
      set f = T --> z;
A13:  f.a = z;
      f.:A = {} by A12;
      hence thesis by A13,XBOOLE_1:2;
    end;
    suppose
      A is non empty;
      then reconsider aa = {a}, A9 = A as non empty closed Subset of T by A11,
URYSOHN1:19;
      reconsider B = A9 \/ aa as closed Subset of T;
      set h = (T|A9 --> j)+*(T|aa --> k);
A14:  T|aa --> k = aa --> k by PRE_TOPC:8;
A15:  (A9 --> 1).:A c= {1} by FUNCOP_1:81;
A16:  a in aa by TARSKI:def 1;
      then
A17:  a in B by XBOOLE_0:def 3;
      assume a in A`;
      then
A18:  not a in A by XBOOLE_0:def 5;
      then A9 misses aa by ZFMISC_1:50;
      then reconsider
      h as continuous Function of T|B, Closed-Interval-TSpace(- 1,1
      ) by Th11;
      consider g being continuous Function of T, Closed-Interval-TSpace(-1,1)
      such that
A19:  g|B = h by A11,TIETZE:23;
      consider p being Function of I[01], Closed-Interval-TSpace(-1,1) such
      that
A20:  p is being_homeomorphism and
      for r being Real st r in [.0,1.] holds p.r=2*r-1 and
A21:  p.0=-1 and
A22:  p.1=1 by JGRAPH_5:39;
      reconsider p9 = p/" as continuous Function of Closed-Interval-TSpace(-1,
      1), I[01] by A20,TOPS_2:def 5;
A23:  p9 = p qua Function" by A20,TOPS_2:def 4;
      then
A24:  p9.k = z by A20,A21,FUNCT_2:26;
A25:  the carrier of T|aa = aa by PRE_TOPC:8;
      then dom (T|aa --> k) = aa;
      then
A26:  h.a = (T|aa --> k).a by A16,FUNCT_4:13
        .= -1 by A25,A16,FUNCOP_1:7;
      reconsider f = p9*g as continuous Function of T, I[01];
A27:  f.:A = p9.:(g.:A) by RELAT_1:126
        .= p9.:(h.:A) by A19,RELAT_1:129,XBOOLE_1:7;
      T|A9 --> j = A9 --> 1 by PRE_TOPC:8;
      then h.:A c= {1} by A14,A15,A18,BOOLMARK:3,ZFMISC_1:50;
      then
A28:  f.:A c= Im(p9,1) by A27,RELAT_1:123;
      take f;
      thus f.a = p9.(g.a) by FUNCT_2:15
        .= 0 by A26,A17,A19,A24,FUNCT_1:49;
      p9.j = o by A20,A22,A23,FUNCT_2:26;
      hence thesis by A28,SETWISEO:8;
    end;
  end;
end;

theorem
  for X being T_1 TopSpace st X is Tychonoff for B being prebasis of X
  for x being Point of X for V being Subset of X st x in V & V in B ex f being
  continuous Function of X, I[01] st f.x = 0 & f.:V` c= {1}
proof
  let X be T_1 TopSpace;
  assume
A1: X is Tychonoff;
  let B be prebasis of X;
  let x be Point of X;
  let V be Subset of X;
  assume that
A2: x in V and
A3: V in B;
A4: V`` = V;
  V is open by A3,TOPS_2:def 1;
  hence thesis by A4,A1,A2;
end;

theorem Th49:
  for X being TopSpace, R being non empty SubSpace of R^1 for f,g
  being continuous Function of X,R for A being Subset of X st for x being Point
  of X holds x in A iff f.x <= g.x holds A is closed
proof
  let X be TopSpace;
  let R be non empty SubSpace of R^1;
  let f,g be continuous Function of X,R;
  let A be Subset of X;
  assume
A1: for x being Point of X holds x in A iff f.x <= g.x;
  now
    thus the topology of X is Basis of X by CANTOR_1:2;
    let p be Point of X;
    set r = f.p-g.p;
    reconsider U1 = ].f.p-r/2,f.p+r/2.[, V1 = ].g.p-r/2,g.p+r/2.[ as open
    Subset of R^1 by JORDAN6:35,TOPMETR:17;
    reconsider U = U1/\[#]R, V = V1/\[#]R as open Subset of R by TOPS_2:24;
A2: g"V is open by TOPS_2:43;
    assume
A3: p in A`;
    then
A4: f.p in [#]R by FUNCT_2:5;
    not p in A by A3,XBOOLE_0:def 5;
    then f.p > g.p by A1;
    then reconsider r as positive Real by XREAL_1:50;
A5: f.p < f.p+r/2 by XREAL_1:29;
    take B = f"U /\ g"V;
A6: g.p < g.p+r/2 by XREAL_1:29;
A7: g.p in [#]R by A3,FUNCT_2:5;
    g.p-r/2 < g.p by XREAL_1:44;
    then g.p in V1 by A6,XXREAL_1:4;
    then g.p in V by A7,XBOOLE_0:def 4;
    then
A8: p in g"V by A3,FUNCT_2:38;
    f.p-r/2 < f.p by XREAL_1:44;
    then f.p in U1 by A5,XXREAL_1:4;
    then f.p in U by A4,XBOOLE_0:def 4;
    then
A9: p in f"U by A3,FUNCT_2:38;
    f"U is open by TOPS_2:43;
    hence B in the topology of X & p in B by A9,A8,A2,PRE_TOPC:def 2
,XBOOLE_0:def 4;
    thus B c= A`
    proof
      let q be object;
       reconsider qq=q as set by TARSKI:1;
      assume
A10:  q in B;
      then q in g"V by XBOOLE_0:def 4;
      then g.q in V by FUNCT_2:38;
      then g.q in V1 by XBOOLE_0:def 4;
      then
A11:  g.qq < g.p+r/2 by XXREAL_1:4;
      q in f"U by A10,XBOOLE_0:def 4;
      then f.q in U by FUNCT_2:38;
      then f.q in U1 by XBOOLE_0:def 4;
      then f.qq > f.p-r/2 by XXREAL_1:4;
      then g.qq < f.qq by A11,XXREAL_0:2;
      then not q in A by A1;
      hence thesis by A10,SUBSET_1:29;
    end;
  end;
  then A` is open by YELLOW_9:31;
  hence thesis;
end;

theorem Th50:
  for X being TopSpace, R being non empty SubSpace of R^1 for f,g
being continuous Function of X,R ex h being continuous Function of X,R st for x
  being Point of X holds h.x = max(f.x,g.x)
proof
  let X be TopSpace;
  let R be non empty SubSpace of R^1;
  let f,g be continuous Function of X,R;
  defpred A[set] means f.$1 >= g.$1;
  consider A being Subset of X such that
A1: for a being set holds a in A iff a in the carrier of X & A[a] from
  SUBSET_1:sch 1;
  defpred B[set] means f.$1 <= g.$1;
  consider B being Subset of X such that
A2: for a being set holds a in B iff a in the carrier of X & B[a] from
  SUBSET_1:sch 1;
  per cases;
  suppose
A3: X is empty;
    set h = the continuous Function of X,R;
    take h;
    let x be Point of X;
A4: f.x = 0 by A3;
A5: g.x = 0 by A3;
    thus thesis by A3,A4,A5;
  end;
  suppose
A6: X is non empty & A is empty;
    take g;
    let x be Point of X;
    f.x < g.x by A6,A1;
    hence thesis by XXREAL_0:def 10;
  end;
  suppose
A7: X is non empty & B is empty;
    take f;
    let x be Point of X;
    g.x < f.x by A7,A2;
    hence thesis by XXREAL_0:def 10;
  end;
  suppose
A8: X is not empty & A is not empty & B is not empty;
    then reconsider X9 = X as non empty TopSpace;
    for x being Point of X9 holds (x in A iff f.x >= g.x) & (x in B iff f
    .x <= g.x) by A1,A2;
    then reconsider A9 = A, B9 = B as non empty closed Subset of X9 by A8,Th49;
    reconsider ff = f, gg = g as continuous Function of X9, R;
A9: the carrier of X9|A9 = [#](X9|A9) .= A9 by PRE_TOPC:def 5;
A10: dom ff = the carrier of X9 by FUNCT_2:def 1;
    then dom (ff|A9) = A9 by RELAT_1:62;
    then reconsider f9 = ff|A9 as continuous Function of X9|A9, R by A9,
FUNCT_2:def 1,RELSET_1:18,TOPMETR:7;
A11: the carrier of X9|B9 = [#](X9|B9) .= B9 by PRE_TOPC:def 5;
A12: dom gg = the carrier of X9 by FUNCT_2:def 1;
    then dom (gg|B9) = B9 by RELAT_1:62;
    then reconsider g9 = gg|B9 as continuous Function of X9|B9, R by A11,
FUNCT_2:def 1,RELSET_1:18,TOPMETR:7;
A13: dom g9 = B by A12,RELAT_1:62;
A14: A9 \/ B9 = the carrier of X9
    proof
      thus A9 \/ B9 c= the carrier of X9;
      let a be object;
       reconsider aa=a as set by TARSKI:1;
      f.aa >= g.aa or f.aa <= g.aa;
      then a in the carrier of X implies a in A9 or a in B9 by A1,A2;
      hence thesis by XBOOLE_0:def 3;
    end;
    then
A15: X9|(A9 \/ B9) = X9 | [#]X9 .= the TopStruct of X by TSEP_1:93;
A16: the TopStruct of R = the TopStruct of R;
A17: dom f9 = A by A10,RELAT_1:62;
A18: f9 tolerates g9
    proof
      let a be object;
      assume
A19:  a in dom f9 /\ dom g9;
      then
A20:  a in A by A17,XBOOLE_0:def 4;
      then
A21:  f.a >= g.a by A1;
A22:  a in B by A19,A13,XBOOLE_0:def 4;
      then f.a <= g.a by A2;
      then f.a = g.a by A21,XXREAL_0:1;
      hence f9.a = g.a by A20,FUNCT_1:49
        .= g9.a by A22,FUNCT_1:49;
    end;
    then f9+*g9 is continuous Function of X9|(A9 \/ B9), R by Th10;
    then reconsider h = f9+*g9 as continuous Function of X,R by A16,A15,
YELLOW12:36;
    take h;
    let x be Point of X;
    x in A9 or x in B9 by A14,XBOOLE_0:def 3;
    then
    x in A9 & f.x >= g.x & h.x = f9.x & f.x = f9.x or x in B9 & f.x <= g.
    x & h.x = g9.x & g.x = g9.x by A1,A17,A13,A18,FUNCT_1:49,FUNCT_4:13,15;
    hence thesis by XXREAL_0:def 10;
  end;
end;

theorem Th51:
  for X being non empty TopSpace, R being non empty SubSpace of
R^1 for A being finite non empty set for F being ManySortedFunction of A st for
  a being set st a in A holds F.a is continuous Function of X,R ex f being
continuous Function of X,R st for x being Point of X, S being finite non empty
  Subset of REAL st S = rng ((commute F).x) holds f.x = max S
proof
  let X be non empty TopSpace;
  let R be non empty SubSpace of R^1;
  let A be finite non empty set;
  let F be ManySortedFunction of A;
  defpred P[set] means $1 is empty or ex f being continuous Function of X,R st
  for x being Point of X, S being finite non empty Subset of REAL st S = rng ((
  commute (F|$1)).x) holds f.x = max S;
A1: P[{}];
A2: dom F = A by PARTFUN1:def 2;
  assume
A3: for a being set st a in A holds F.a is continuous Function of X,R;
  rng F c= Funcs(the carrier of X,the carrier of R)
  proof
    let a be object;
    assume a in rng F;
    then ex b being object st b in dom F & a = F.b by FUNCT_1:def 3;
    then a is Function of X,R by A3;
    hence thesis by FUNCT_2:8;
  end;
  then
A4: F in Funcs(A,Funcs(the carrier of X,the carrier of R)) by A2,FUNCT_2:def 2;
A5: now
    let x,B be set;
    assume
A6: x in A;
    then reconsider fx = F.x as continuous Function of X,R by A3;
    assume
A7: B c= A;
    assume
A8: P[B];
    per cases;
    suppose
A9:  B = {};
      thus P[B \/ {x}]
      proof
        assume B \/ {x} is not empty;
        take fx;
        let a be Point of X, S be finite non empty Subset of REAL;
A10:    dom fx = the carrier of X by FUNCT_2:def 1;
        F|{x} = x .--> (F.x) by A2,A6,FUNCT_7:6;
        then (commute (F|{x})).a = x .--> (fx.a) by A10,Th3;
        then
A11:    rng ((commute (F|{x})).a) = {fx.a} by FUNCOP_1:8;
        assume S = rng ((commute (F|(B \/ {x}))).a);
        hence thesis by A11,A9,XXREAL_2:11;
      end;
    end;
    suppose
A12:  B <> {};
      then reconsider B9 = B as non empty set;
      consider f being continuous Function of X,R such that
A13:  for x being Point of X, S being finite non empty Subset of REAL
      st S = rng ((commute (F|B9)).x) holds f.x = max S by A8;
      consider h being continuous Function of X,R such that
A14:  for x being Point of X holds h.x = max(f.x,fx.x) by Th50;
      thus P[B \/ {x}]
      proof
        F is Function of A, Funcs(the carrier of X,the carrier of R) by A4,
FUNCT_2:66;
        then
        F|B is Function of B, Funcs(the carrier of X,the carrier of R) by A7,
FUNCT_2:32;
        then F|B in Funcs(B, Funcs(the carrier of X,the carrier of R)) by
FUNCT_2:8;
        then commute (F|B) in Funcs(the carrier of X, Funcs(B, the carrier of
        R)) by A12,FUNCT_6:55;
        then reconsider
        cFB = commute (F|B) as Function of the carrier of X, Funcs(
        B, the carrier of R) by FUNCT_2:66;
        assume B \/ {x} is not empty;
        take h;
        let a be Point of X, S be finite non empty Subset of REAL;
        reconsider cFBa = cFB.a as Function of B9, the carrier of R;
A15:    dom fx = the carrier of X by FUNCT_2:def 1;
        F|(B \/ {x}) = (F|B) \/ (F|{x}) by RELAT_1:78;
        then
A16:    (commute (F|(B\/{x}))).a = cFB.a \/ (commute (F|{x})).a by Th7;
        assume S = rng ((commute (F|(B \/ {x}))).a);
        then
A17:    S = rng cFBa \/ rng ((commute (F|{x})).a) by A16,RELAT_1:12;
        then rng cFBa c= S by XBOOLE_1:7;
        then reconsider S1 = rng cFBa as non empty finite Subset of REAL by
XBOOLE_1:1;
        F|{x} = x .--> (F.x) by A2,A6,FUNCT_7:6;
        then (commute (F|{x})).a = x .--> (fx.a) by A15,Th3;
        then
A18:    S = S1 \/ {fx.a} by A17,FUNCOP_1:8;
        f.a = max S1 by A13;
        then max S = max(f.a, max {fx.a}) by A18,XXREAL_2:10
          .= max(f.a, fx.a) by XXREAL_2:11;
        hence thesis by A14;
      end;
    end;
  end;
A19: A is finite;
  P[A] from FINSET_1:sch 2(A19,A1,A5);
  hence thesis;
end;

theorem Th52:
  for X being T_1 non empty TopSpace for B being prebasis of X st
  for x being Point of X for V being Subset of X st x in V & V in B ex f being
continuous Function of X, I[01] st f.x = 0 & f.:V` c= {1} holds X is Tychonoff
proof
  reconsider z = 0 as Point of I[01] by BORSUK_1:40,XXREAL_1:1;
  let X be T_1 non empty TopSpace;
  let BB be prebasis of X such that
A1: for x being Point of X for V being Subset of X st x in V & V in BB
  ex f being continuous Function of X, I[01] st f.x = 0 & f.:V` c= {1};
  let A be closed Subset of X;
  let a be Point of X;
A2: FinMeetCl BB is Basis of X by YELLOW_9:23;
  assume a in A`;
  then consider B being Subset of X such that
A3: B in FinMeetCl BB and
A4: a in B and
A5: B c= A` by A2,YELLOW_9:31;
  consider F being Subset-Family of X such that
A6: F c= BB and
A7: F is finite and
A8: B = Intersect F by A3,CANTOR_1:def 3;
  per cases;
  suppose
    F is empty;
    then B = the carrier of X by A8,SETFAM_1:def 9;
    then A`` = {}X by A5,XBOOLE_1:37;
    then
A9: (X-->z).:A = {};
    (X-->z).a = z;
    hence thesis by A9,XBOOLE_1:2;
  end;
  suppose
    F is non empty;
    then reconsider F as finite non empty Subset-Family of X by A7;
    defpred P[object,object] means
   ex S being Subset of X, f being continuous
    Function of X, I[01] st S = $1 & f = $2 & f.a = 0 & f.:S` c= {1};
    reconsider Sa = {In(0,REAL)}
           as finite non empty Subset of REAL;
    set z = the Element of F;
    set R = I[01];
A10: for x being object st x in F ex y being object st P[x,y]
    proof
      let x be object;
      assume
A11:  x in F;
      then reconsider S = x as Subset of X;
      a in S by A4,A8,A11,SETFAM_1:43;
      then consider f being continuous Function of X, I[01] such that
A12:  f.a = 0 and
A13:  f.:S` c= {1} by A6,A11,A1;
      take f;
      thus thesis by A12,A13;
    end;
    consider G being Function such that
A14: dom G = F & for x being object st x in F holds P[x,G.x] from
    CLASSES1:sch 1(A10);
    G is Function-yielding
    proof
      let x be object;
      assume x in dom G;
      then P[x,G.x] by A14;
      hence thesis;
    end;
    then reconsider G as ManySortedFunction of F by A14,PARTFUN1:def 2
,RELAT_1:def 18;
    rng G c= Funcs(the carrier of X,the carrier of R)
    proof
      let u be object;
      assume u in rng G;
      then consider v being object such that
A15:  v in dom G and
A16:  u = G.v by FUNCT_1:def 3;
      P[v,u] by A14,A15,A16;
      hence thesis by FUNCT_2:8;
    end;
    then G is Function of F, Funcs(the carrier of X,the carrier of R) by A14,
FUNCT_2:2;
    then
A17: G in Funcs(F, Funcs(the carrier of X,the carrier of R)) by FUNCT_2:8;
    then commute G in Funcs(the carrier of X, Funcs(F, the carrier of R)) by
FUNCT_6:55;
    then reconsider
    cG = commute G as Function of the carrier of X, Funcs(F, the
    carrier of R) by FUNCT_2:66;
    now
      let a be set;
      assume a in F;
      then P[a,G.a] by A14;
      hence G.a is continuous Function of X, I[01];
    end;
    then consider f being continuous Function of X, I[01] such that
A18: for x being Point of X, S being finite non empty Subset of REAL
    st S = rng ((commute G).x) holds f.x = max S by Th51;
    take f;
    reconsider cGa = cG.a as Function of F, the carrier of R;
A19: dom cGa = F by FUNCT_2:def 1;
    Sa = rng ((commute G).a)
    proof
      thus Sa c= rng ((commute G).a)
      proof
        let x be object;
        assume x in Sa;
        then
A20:    x = 0 by TARSKI:def 1;
        P[z,G.z] by A14;
        then x = (commute G).a.z by A20,A17,FUNCT_6:56;
        hence thesis by A19,FUNCT_1:def 3;
      end;
      let x be object;
      assume x in rng ((commute G).a);
      then consider z being object such that
A21:  z in dom cGa and
A22:  x = cGa.z by FUNCT_1:def 3;
      P[z,G.z] by A14,A21;
      then x = 0 by A17,A21,A22,FUNCT_6:56;
      hence thesis by TARSKI:def 1;
    end;
    hence f.a = max Sa by A18
      .= 0 by XXREAL_2:11;
    let z be object;
    assume z in f.:A;
    then consider x being object such that
A23: x in dom f and
A24: x in A and
A25: z = f.x by FUNCT_1:def 6;
    reconsider x as Element of X by A23;
    not x in B by A5,A24,XBOOLE_0:def 5;
    then consider w such that
A26: w in F and
A27: not x in w by A8,SETFAM_1:43;
    reconsider cGx = cG.x as Function of F, the carrier of R;
    reconsider S = rng cGx as finite non empty Subset of REAL by BORSUK_1:40
,XBOOLE_1:1;
A28: f.x = max S by A18;
    consider T being Subset of X, g being continuous Function of X, R such
    that
A29: T = w and
A30: g = G.w and
    g.a = 0 and
A31: g.:T` c= {1} by A14,A26;
    x in T` by A27,A29,SUBSET_1:29;
    then g.x in g.:T` by FUNCT_2:35;
    then g.x = 1 by A31,TARSKI:def 1;
    then
A32: cGx.w = 1 by A17,A26,A30,FUNCT_6:56;
    w in dom cGx by A17,A26,A30,FUNCT_6:56;
    then
A33: 1 in S by A32,FUNCT_1:def 3;
    for r being ExtReal st r in S holds r <= 1 by BORSUK_1:40,XXREAL_1:1;
    then max S = 1 by A33,XXREAL_2:def 8;
    hence thesis by A25,A28,TARSKI:def 1;
  end;
end;

theorem Th53:
  Sorgenfrey-line is T_1
proof
  set T = Sorgenfrey-line;
  consider B being Subset-Family of REAL such that
A1: the topology of Sorgenfrey-line = UniCl B and
A2: B = {[.x,q.[ where x,q is Real: x < q & q is rational}
     by TOPGEN_3:def 2;
  let x,y be Point of T;
  reconsider a = x, b = y as Element of REAL by TOPGEN_3:def 2;
A3: B c= the topology of T by A1,CANTOR_1:1;
  assume
A4: x <> y;
  per cases by A4,XXREAL_0:1;
  suppose
A5: a < b;
    b < b+1 by XREAL_1:29;
    then consider q being Rational such that
A6: b < q and
    q < b+1 by RAT_1:7;
    [.b,q.[ in B by A2,A6;
    then
A7: [.b,q.[ in the topology of T by A3;
    consider w being Rational such that
A8: a < w and
A9: w < b by A5,RAT_1:7;
    [.a,w.[ in B by A2,A8;
    then [.a,w.[ in the topology of T by A3;
    then reconsider U = [.a,w.[, V = [.b,q.[ as open Subset of T by A7,
PRE_TOPC:def 2;
    take U,V;
    thus U is open & V is open;
    thus thesis by A5,A8,A9,A6,XXREAL_1:3;
  end;
  suppose
A10: a > b;
    a < a+1 by XREAL_1:29;
    then consider q being Rational such that
A11: a < q and
    q < a+1 by RAT_1:7;
    [.a,q.[ in B by A2,A11;
    then
A12: [.a,q.[ in the topology of T by A3;
    consider w being Rational such that
A13: b < w and
A14: w < a by A10,RAT_1:7;
    [.b,w.[ in B by A2,A13;
    then [.b,w.[ in the topology of T by A3;
    then reconsider V = [.b,w.[, U = [.a,q.[ as open Subset of T by A12,
PRE_TOPC:def 2;
    take U,V;
    thus U is open & V is open;
    thus thesis by A10,A13,A14,A11,XXREAL_1:3;
  end;
end;

theorem Th54:
  for x being Real holds left_open_halfline x is closed
  Subset of Sorgenfrey-line
proof
  let x be Real;
  set T = Sorgenfrey-line;
  reconsider A = right_closed_halfline x as open Subset of T by TOPGEN_3:15;
  the carrier of T = REAL by TOPGEN_3:def 2;
  then left_open_halfline x = A` by XXREAL_1:224,294;
  hence thesis;
end;

theorem
  for x being Real holds left_closed_halfline x is closed Subset
  of Sorgenfrey-line
proof
  let x be Real;
  set T = Sorgenfrey-line;
  reconsider A = right_open_halfline x as open Subset of T by TOPGEN_3:14;
  the carrier of T = REAL by TOPGEN_3:def 2;
  then (left_closed_halfline x)`` = A` by XXREAL_1:224,288;
  hence thesis;
end;

theorem Th56:
  for x being Real holds right_closed_halfline x is closed
  Subset of Sorgenfrey-line
proof
  let x be Real;
  set T = Sorgenfrey-line;
  reconsider A = left_open_halfline x as open Subset of T by TOPGEN_3:13;
  the carrier of T = REAL by TOPGEN_3:def 2;
  then (right_closed_halfline x)`` = A` by XXREAL_1:224,294;
  hence thesis;
end;

theorem Th57:
  for x,y being Real holds [.x,y.[ is closed Subset of Sorgenfrey-line
proof
  let x,y be Real;
  set T = Sorgenfrey-line;
  reconsider A = right_closed_halfline x, B = left_open_halfline y as closed
  Subset of T by Th54,Th56;
A1: the carrier of T = REAL by TOPGEN_3:def 2;
  [.x,y.[ = [.x,y.[``
    .= (left_open_halfline(x) \/ right_closed_halfline(y))` by XXREAL_1:382
    .= (left_open_halfline x)` /\ (right_closed_halfline y)` by XBOOLE_1:53
    .= A`` /\ (right_closed_halfline y)` by A1,XXREAL_1:224,294
    .= A /\ B by XXREAL_1:224,294;
  hence thesis;
end;

::<DESC name="1.4.4. Przyk/lad funkcji ci/ag/lej ze strza/lce w [0,1]" monograph="topology"/>

theorem Th58:
  for x being Real, w being Rational ex f being
  continuous Function of Sorgenfrey-line, I[01] st for a being Point of
  Sorgenfrey-line holds (a in [.x,w.[ implies f.a = 0) & (not a in [.x,w.[
  implies f.a = 1)
proof
  reconsider 00 = 0, 01 = 1 as Element of I[01] by BORSUK_1:40,XXREAL_1:1;
  let x be Real;
  set X = Sorgenfrey-line;
  let w be Rational;
  reconsider V = [.x,w.[ as open closed Subset of X by Th57,TOPGEN_3:11;
  defpred P[object] means $1 in [.x,w.[;
  deffunc 00(object) = 0;
  deffunc 01(object) = 1;
   :: funkcja charakterystyczna zbioru [.x,w.[ !!! ???
  reconsider f1 = (X|V) --> 00 as continuous Function of X|V, I[01];
  reconsider f2 = (X|V`) --> 01 as continuous Function of X|V`, I[01];
A1: for a being object st a in the carrier of X holds (P[a] implies 00(a) in
  the carrier of I[01]) & (not P[a] implies 01(a) in the carrier of I[01]) by
BORSUK_1:40,XXREAL_1:1;
  consider f being Function of X, I[01] such that
A2: for a being object st a in the carrier of X holds (P[a] implies f.a =
  00(a)) & (not P[a] implies f.a = 01(a)) from FUNCT_2:sch 5(A1);
 the carrier of X|V = V by PRE_TOPC:8;
  then
A4: dom f1 = V;
A5: the carrier of X|V` = V` by PRE_TOPC:8;
  then
A6: dom f2 = V`;
A7: dom f = [#]X by FUNCT_2:def 1;
A8: now
    let u be object;
    assume u in dom f1 \/ dom f2;
    then reconsider x = u as Point of X by A7,A4,A6,PRE_TOPC:2;
    hereby
      assume
A9:   u in dom f2;
      then
A10:  (V`-->1).u = 1 by A5,FUNCOP_1:7;
      not x in V by A9,A5,XBOOLE_0:def 5;
      hence f.u = f2.u by A10,A5,A2;
    end;
    assume not u in dom f2;
    then
 x in V by A6,SUBSET_1:29;
    hence f.u = 0 by A2
      .= f1.u;
  end;
  V \/ V` = [#]X by PRE_TOPC:2;
  then f = f1+*f2 by A8,A7,A4,A6,FUNCT_4:def 1;
  then reconsider f as continuous Function of Sorgenfrey-line, I[01] by Th12;
  take f;
  let a be Point of Sorgenfrey-line;
  thus thesis by A2;
end;

theorem
  Sorgenfrey-line is Tychonoff
proof
  set X = Sorgenfrey-line;
A1: the carrier of X = REAL by TOPGEN_3:def 2;
  consider B being Subset-Family of REAL such that
A2: the topology of X = UniCl B and
A3: B = {[.x,q.[ where x,q is Real: x < q & q is rational}
    by TOPGEN_3:def 2;
  B c= UniCl B by CANTOR_1:1;
  then B is Basis of X by A1,A2,CANTOR_1:def 2,TOPS_2:64;
  then reconsider B as prebasis of X by YELLOW_9:27;
  now
    let x be Point of X;
    let V be Subset of X;
    assume that
A4: x in V and
A5: V in B;
    consider a,q being Real such that
A6: V = [.a,q.[ and
    a < q and
A7: q is rational by A5,A3;
    consider f being continuous Function of X, I[01] such that
A8: for b being Point of Sorgenfrey-line holds (b in [.a,q.[ implies
    f.b = 0) & (not b in [.a,q.[ implies f.b = 1) by A7,Th58;
    take f;
    thus f.x = 0 by A4,A6,A8;
    thus f.:V` c= {1}
    proof
      let u be object;
      assume u in f.:V`;
      then consider b being Point of X such that
A9:   b in V` and
A10:  u = f.b by FUNCT_2:65;
      not b in [.a,q.[ by A6,A9,XBOOLE_0:def 5;
      then u = 1 by A8,A10;
      hence thesis by TARSKI:def 1;
    end;
  end;
  hence thesis by Th52,Th53;
end;

begin :: Niemytzki plane is Tychonoff space
::<DESC name="1.4.5. Przyk/lad funkcji ci/ag/lej z p/laszczyzny Niemytzkiego w R^1" monograph="topology"/>

definition
  let x be Real, r be positive Real;
  func +(x,r) -> Function of Niemytzki-plane, I[01] means
  :Def5:
  it.(|[x,0]|)
= 0 & for a being Real, b being non negative Real holds ((a <>
x or b <> 0) & not |[a,b]| in Ball(|[x,r]|,r) implies it.(|[a,b]|) = 1) & (|[a,
  b]| in Ball(|[x,r]|,r) implies it.(|[a,b]|) = |.|[x,0]|-|[a,b]|.|^2/(2*r*b));
  existence
  proof
    deffunc F3(Point of TOP-REAL 2) = |.|[x,0]|-$1.|^2/(2*r*$1`2);
    deffunc F2(Point of TOP-REAL 2) = 1;
    deffunc F1(Point of TOP-REAL 2) = 0;
    defpred Q[set] means not $1 in Ball(|[x,r]|, r);
    defpred P[set] means $1 = |[x,0]|;
A1: for a being Point of TOP-REAL 2 st a in the carrier of Niemytzki-plane
holds (P[a] implies F1(a) in the carrier of I[01]) & (not P[a] & Q[a] implies
    F2(a) in the carrier of I[01]) & (not P[a] & not Q[a] implies F3(a) in the
    carrier of I[01])
    proof
      let a be Point of TOP-REAL 2;
      assume a in the carrier of Niemytzki-plane;
      thus P[a] implies F1(a) in the carrier of I[01] by BORSUK_1:40,XXREAL_1:1
;
      thus not P[a] & Q[a] implies F2(a) in the carrier of I[01] by BORSUK_1:40
,XXREAL_1:1;
      assume not P[a];
A2:   a = |[a`1,a`2]| by EUCLID:53;
      assume not Q[a];
      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 F3(a) <= 1 by XREAL_1:183;
      hence thesis by A7,BORSUK_1:40,XXREAL_1:1;
    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 (P[a] implies f.a = F1(a)) & (not P[a] & Q[a] implies f.a
    = F2(a)) & (not P[a] & not Q[a] implies f.a = F3(a)) from SCH2(A8,A1);
    take f;
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;
    let a be Real, b be non negative Real;
A11: |[a,b]| in the carrier of Niemytzki-plane by A10;
    hereby
      assume a <> x or b <> 0;
      then not P[ |[a,b]| ] by SPPOL_2:1;
      hence not |[a,b]| in Ball(|[x,r]|,r) implies f.(|[a,b]|) = 1 by A9,A11;
    end;
    assume
A12: |[a,b]| in Ball(|[x,r]|,r);
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 P[ |[a,b]| ] by A13,A12,XBOOLE_0:3;
    hence thesis by A14,A9,A11,A12;
  end;
  uniqueness
  proof
    let f,g be Function of Niemytzki-plane, I[01] such that
A15: f.(|[x,0]|) = 0 and
A16: for a being Real, 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)
    ) and
A17: g.(|[x,0]|) = 0 and
A18: for a being Real, b being non negative Real holds
((a <> x or b <> 0) & not |[a,b]| in Ball(|[x,r]|,r) implies g.(|[a,b]|) = 1) &
(|[a,b]| in Ball(|[x,r]|,r) implies g.(|[a,b]|) = |.|[x,0]|-|[a,b]|.|^2/(2*r*b)
    );
A19: the carrier of Niemytzki-plane = y>=0-plane by Def3;
    now
      let p be Point of Niemytzki-plane;
      p in y>=0-plane by A19;
      then reconsider q = p as Point of TOP-REAL 2;
A20:  p = |[q`1,q`2]| by EUCLID:53;
      then reconsider q2 = q`2 as non negative Real by A19,Th18;
      per cases by EUCLID:53;
      suppose
        q`1 = x & q2 = 0;
        hence f.p = g.p by A15,A17,A20;
      end;
      suppose
A21:    (q`1 <> x or q2 <> 0) & not |[q`1,q2]| in Ball(|[x,r]|,r);
        then f.p = 1 by A16,A20;
        hence f.p = g.p by A18,A20,A21;
      end;
      suppose
A22:    p in Ball(|[x,r]|,r);
        then f.p = |.|[x,0]|-q.|^2/(2*r*q2) by A16,A20;
        hence f.p = g.p by A18,A20,A22;
      end;
    end;
    hence thesis;
  end;
end;

theorem Th60:
  for p being Point of TOP-REAL 2 st p`2 >= 0 for x being Real
, r being positive Real st +(x,r).p = 0 holds p = |[x,0]|
proof
  let p be Point of TOP-REAL 2;
  assume
A1: p`2 >= 0;
  set p1 = p`1, p2 = p`2;
  let x be Real;
  let r be positive Real;
  assume
A2: +(x,r).p = 0;
A3: p = |[p1,p2]| by EUCLID:53;
  assume
A4: p <> |[x,0]|;
  then p1 <> x or p2 <> 0 by EUCLID:53;
  then
A5: |[p1,p2]| in Ball(|[x,r]|,r) by A1,A2,A3,Def5;
  Ball(|[x,r]|,r) misses y=0-line by Th21;
  then not |[p1,p2]| in y=0-line by A5,XBOOLE_0:3;
  then p2 <> 0;
  then reconsider p2 as positive Real by A1;
  0/(2*r*p2) = |.|[x,0]|-|[p1,p2]|.|^2/(2*r*p2) by A2,A3,A5,Def5;
  then 0 = |.|[x,0]|-p.| by A3;
  hence contradiction by A4,TOPRNS_1:28;
end;

theorem Th61:
  for x,y being Real, r being positive Real st x
  <> y holds +(x,r).(|[y,0]|) = 1
proof
  let x,y be Real;
  let r be positive Real;
A1: |.x-y.| = x-y or |.x-y.| = - (x-y) by ABSVALUE:1;
A2: |[x-y,r]|`2 = r by EUCLID:52;
  |[x-y,r]|`1 = x-y by EUCLID:52;
  then
A3: |.|[x-y,r]|.|^2 = r^2+(x-y)^2 by A2,JGRAPH_1:29;
  assume
A4: x <> y;
  then x-y <> 0;
  then
A5: |.x-y.| > 0 by COMPLEX1:47;
  then |.x-y.|^2 <> 0;
  then |.|[x-y,r]|.|^2 > r^2 by A1,A5,A3,XREAL_1:29;
  then |.|[x-y,r-0]|.| > r by SQUARE_1:15;
  then |.|[x,r]|-|[y,0]|.| > r by EUCLID:62;
  then |.|[y,0]|-|[x,r]|.| > r by TOPRNS_1:27;
  then not |[y,0]| in Ball(|[x,r]|,r) by TOPREAL9:7;
  hence thesis by A4,Def5;
end;

theorem Th62:
  for p being Point of TOP-REAL 2 for x being Real, a,r
being positive Real st a <= 1 & |.p-|[x,r*a]|.| = r*a & p`2 <> 0 holds
  +(x,r).p = a
proof
  let p be Point of TOP-REAL 2;
  set p1 = p`1, p2 = p`2;
  let x be Real;
  let a,r be positive Real;
  assume
A1: a <= 1;
A2: |[p1-x,p2-r*a]|`1 = p1-x by EUCLID:52;
A3: |[p1-x,p2-r*a]|`2 = p2-r*a by EUCLID:52;
  assume that
A4: |.p-|[x,r*a]|.| = r*a and
A5: p`2 <> 0;
A6: p = |[p`1,p`2]| by EUCLID:53;
  then |.|[p1-x,p2-r*a]|.|^2 = (r*a)^2 by A4,EUCLID:62;
  then
A7: (p1-x)^2+(p2-r*a)^2 = (r*a)^2 by A2,A3,JGRAPH_1:29;
  then
A8: (p1-x)^2+p2^2 = 2*p2*r*a;
  (p1-x)^2 >= 0 by XREAL_1:63;
  then reconsider p2 as positive Real by A5,A8;
A9: |[p1-x,p2-0]|`1 = p1-x by EUCLID:52;
A10: |[p1-x,p2]|`2 = p2 by EUCLID:52;
  per cases by A1,XXREAL_0:1;
  suppose
    a < 1;
    then r*a < r by XREAL_1:157;
    then reconsider s = r-r*a as positive Real by XREAL_1:50;
    |.p-|[x,r]|.|^2 = |.|[p1-x,p2-r]|.|^2 by A6,EUCLID:62
      .= (p1-x)^2+(p2-r)^2 by Th9
      .= (p1-x)^2+(p2-a*r)^2+((r-a*r)^2+2*(r-a*r)*(a*r-p2))
      .= |.|[p1-x,p2-a*r]|.|^2+((r-a*r)^2+2*(r-a*r)*(a*r-p2)) by Th9
      .= (a*r)^2+(r*r-r*p2+r*a*r-r*p2-(a*r*r-a*r*p2+(a*r)^2-a*r*p2)) by A6,A4,
EUCLID:62
      .= r^2-(1+1)*p2*s;
    then |.p-|[x,r]|.|^2 < r^2 by XREAL_1:44;
    then |.p-|[x,r]|.| < r by SQUARE_1:15;
    then p in Ball(|[x,r]|,r) by TOPREAL9:7;
    then +(x,r).p = |.|[x,0]|-p.|^2/(2*r*p2) by A6,Def5
      .= |.p-|[x,0]|.|^2/(2*r*p2) by TOPRNS_1:27
      .= |.|[p1-x,p2-0]|.|^2/(2*r*p2) by A6,EUCLID:62
      .= ((p1-x)^2+p2^2)/(2*r*p2) by A9,A10,JGRAPH_1:29;
    then
A11: +(x,r).p = (2*p2*r*a)/(2*r*p2) by A7;
    a*((2*p2*r)/(2*r*p2)) = a*1 by XCMPLX_1:60;
    hence thesis by A11,XCMPLX_1:74;
  end;
  suppose
A12: a = 1;
A13: p2 is non negative;
    not p in Ball(|[x,r]|,r) by A12,A4,TOPREAL9:7;
    hence thesis by A13,A6,A12,Def5;
  end;
end;

theorem Th63:
  for p being Point of TOP-REAL 2 for x,a being Real, r
being positive Real st a <= 1 & |.p-|[x,r*a]|.| < r*a holds +(x,r).p <
  a
proof
  let p be Point of TOP-REAL 2;
  set p1 = p`1, p2 = p`2;
  let x,a be Real;
  let r be positive Real;
  assume that
A1: a <= 1;
A2: |[p1-x,p2-r*a]|`2 = p2-r*a by EUCLID:52;
A3: p = |[p`1,p`2]| by EUCLID:53;
  then
A4: p2 = 0 implies p in y=0-line;
  set r1 = r*a, r2 = r*1;
A5: |[p1-x,p2-r*a]|`1 = p1-x by EUCLID:52;
  assume
A6: |.p-|[x,r*a]|.| < r*a;
  then reconsider r1 as positive Real;
A7: p in Ball(|[x,r1]|,r1) by A6,TOPREAL9:7;
  |.p-|[x,r*a]|.|^2 < (r*a)^2 by A6,SQUARE_1:16;
  then |.|[p1-x,p2-r*a]|.|^2 < (r*a)^2 by A3,EUCLID:62;
  then (p1-x)^2+(p2-r*a)^2 < (r*a)^2 by A5,A2,JGRAPH_1:29;
  then (p1-x)^2+p2^2-2*p2*(r*a)+(r*a)^2 < (r*a)^2;
  then (p1-x)^2+p2^2-2*p2*r*a < 0 by XREAL_1:31;
  then
A8: (p1-x)^2+p2^2 < 2*p2*r*a by XREAL_1:48;
A9: Ball(|[x,r1]|,r1) misses y=0-line by Th21;
  Ball(|[x,r1]|,r1) c= y>=0-plane by Th20;
  then reconsider p2 as positive Real by A3,A7,Th18,A9,A4,XBOOLE_0:3;
A10: |[p1-x,p2-0]|`1 = p1-x by EUCLID:52;
A11: |[p1-x,p2]|`2 = p2 by EUCLID:52;
  Ball(|[x,r1]|,r1) c= Ball(|[x,r2]|,r2) by A1,Th23,XREAL_1:64;
  then +(x,r).p = |.|[x,0]|-p.|^2/(2*r*p2) by A3,A7,Def5
    .= |.p-|[x,0]|.|^2/(2*r*p2) by TOPRNS_1:27
    .= |.|[p1-x,p2-0]|.|^2/(2*r*p2) by A3,EUCLID:62
    .= ((p1-x)^2+p2^2)/(2*r*p2) by A10,A11,JGRAPH_1:29;
  then
A12: +(x,r).p < (2*p2*r*a)/(2*r*p2) by A8,XREAL_1:74;
  a*((2*p2*r)/(2*r*p2)) = a*1 by XCMPLX_1:60;
  hence thesis by A12,XCMPLX_1:74;
end;

theorem Th64:
  for p being Point of TOP-REAL 2 st p`2 >= 0 for x,a being Real
, r being positive Real st 0 <= a & a < 1 & |.p-|[x,r*a]|.| > r*
  a holds +(x,r).p > a
proof
  let p be Point of TOP-REAL 2 such that
A1: p`2 >= 0;
  set p1 = p`1, p2 = p`2;
  reconsider p2 as non negative Real by A1;
  let x,a be Real;
  let r be positive Real;
  assume that
A2: 0 <= a and
A3: a < 1;
  reconsider a9 = a as non negative Real by A2;
  reconsider ra = r*a as Real;
  assume
A4: |.p-|[x,r*a]|.| > r*a;
  |.|[x,0]|-|[x,r*a]|.| = |.|[x,r*a]|-|[x,0]|.| by TOPRNS_1:27
    .= |.|[x-x,ra-0]|.| by EUCLID:62
    .= |.ra.| by TOPREAL6:23
    .= r*a9 by ABSVALUE:def 1;
  then
A5: p1 <> x or p2 <> 0 by A4,EUCLID:53;
A6: p = |[p`1,p`2]| by EUCLID:53;
  then reconsider z = p as Element of Niemytzki-plane by A1,Lm1,Th18;
A7: +(x,r).z in the carrier of I[01];
  per cases by A2;
  suppose
A8: a = 0;
    then p <> |[x,r*0]| by A4,TOPRNS_1:28;
    then +(x,r).p <> 0 by A1,Th60;
    hence thesis by A7,A8,BORSUK_1:40,XXREAL_1:1;
  end;
  suppose
    +(x,r).p = 1;
    hence thesis by A3;
  end;
  suppose
A9: a > 0 & +(x,r).z <> 1;
A10: |[p1-x,p2-0]|`1 = p1-x by EUCLID:52;
A11: |[p1-x,p2]|`2 = p2 by EUCLID:52;
    p2 is non negative;
    then
A12: p in Ball(|[x,r]|,r) by A6,A5,A9,Def5;
    then
A13: +(x,r).p = |.|[x,0]|-p.|^2/(2*r*p2) by A6,Def5
      .= |.p-|[x,0]|.|^2/(2*r*p2) by TOPRNS_1:27
      .= |.|[p1-x,p2-0]|.|^2/(2*r*p2) by A6,EUCLID:62
      .= ((p1-x)^2+p2^2)/(2*r*p2) by A10,A11,JGRAPH_1:29;
    |.p-|[x,r*a]|.|^2 > (r*a)^2 by A2,A4,SQUARE_1:16;
    then
A14: |.|[p1-x,p2-r*a]|.|^2 > (r*a)^2 by A6,EUCLID:62;
A15: |[p1-x,p2-r*a]|`2 = p2-r*a by EUCLID:52;
    |[p1-x,p2-r*a]|`1 = p1-x by EUCLID:52;
    then (p1-x)^2+(p2-r*a)^2 > (r*a)^2 by A14,A15,JGRAPH_1:29;
    then (p1-x)^2+p2^2-2*p2*(r*a)+(r*a)^2 > (r*a)^2;
    then (p1-x)^2+p2^2-2*p2*r*a > 0 by XREAL_1:32;
    then
A16: (p1-x)^2+p2^2 > 2*p2*r*a by XREAL_1:47;
A17: p2 = 0 implies p in y=0-line by A6;
    Ball(|[x,r]|,r) misses y=0-line by Th21;
    then reconsider p2 as positive Real by A12,A17,XBOOLE_0:3;
A18: a*((2*p2*r)/(2*r*p2)) = a*1 by XCMPLX_1:60;
    +(x,r).p > (2*p2*r*a)/(2*r*p2) by A13,A16,XREAL_1:74;
    hence thesis by A18,XCMPLX_1:74;
  end;
end;

theorem Th65:
  for p being Point of TOP-REAL 2 st p`2 >= 0 for x,a,b being Real
, r being positive Real st 0 <= a & b <= 1 & +(x,r).p in ].a,b.[
ex r1 being positive Real st r1 <= p`2 & Ball(p,r1) c= +(x,r)"].a,b.[
proof
  let p be Point of TOP-REAL 2 such that
A1: p`2 >= 0;
  let x,a,b be Real, r be positive Real;
A2: p = |[p`1,p`2]| by EUCLID:53;
A3: Ball(|[x,r]|,r) misses y=0-line by Th21;
A4: |[p`1-x,p`2]|`1 = p`1-x by EUCLID:52;
  assume that
A5: 0 <= a and
A6: b <= 1 and
A7: +(x,r).p in ].a,b.[;
A8: +(x,r).p > a by A7,XXREAL_1:4;
A9: +(x,r).p < b by A7,XXREAL_1:4;
  then
A10: p in Ball(|[x,r]|,r) or p`1 = x & p`2 = 0 & p <> |[x,0]| by A8,A1,A2,A5,A6
,Def5;
  then
A11: +(x,r).p = |.|[x,0]|-p.|^2/(2*r*p`2) by A1,A2,Def5;
  p`2 = 0 implies p in y=0-line by A2;
  then reconsider p2 = p`2, b9 = b as positive Real by A3,A1,A5,A8,A7,A10,
EUCLID:53,XBOOLE_0:3,XXREAL_1:4;
A12: |[p`1-x,p2]|`2 = p2 by EUCLID:52;
A13: 2*r*p2 > 0;
  then |.|[x,0]|-p.|^2 > (2*r*p`2)*a by A11,A8,XREAL_1:79;
  then |.p-|[x,0]|.|^2 > (2*r*p`2)*a by TOPRNS_1:27;
  then |.|[p`1-x,p`2-0]|.|^2 > (2*r*p`2)*a by A2,EUCLID:62;
  then (p`1-x)^2+p2^2 > (2*r*p2)*a by A4,A12,JGRAPH_1:29;
  then (p`1-x)^2+p2^2 - (2*r*p2)*a > 0 by XREAL_1:50;
  then (p`1-x)^2+p2^2 - (2*r*p2)*a + (r*a)^2 > (r*a)^2 by XREAL_1:29;
  then
A14: (p`1-x)^2+(p2 - r*a)^2 > (r*a)^2;
  |.|[x,0]|-p.|^2 < (2*r*p`2)*b by A13,A11,A9,XREAL_1:77;
  then |.p-|[x,0]|.|^2 < (2*r*p`2)*b by TOPRNS_1:27;
  then |.|[p`1-x,p`2-0]|.|^2 < (2*r*p`2)*b by A2,EUCLID:62;
  then (p`1-x)^2+p2^2 < (2*r*p2)*b by A4,A12,JGRAPH_1:29;
  then (p`1-x)^2+p2^2 - (2*r*p2)*b < 0 by XREAL_1:49;
  then (p`1-x)^2+p2^2 - (2*r*p2)*b + (r*b)^2 < (r*b)^2 by XREAL_1:30;
  then
A15: (p`1-x)^2+(p2 - r*b)^2 < (r*b)^2;
A16: |[p`1-x, p2-r*b]|`2 = p2-r*b by EUCLID:52;
A17: |[p`1-x, p2-r*a]|`2 = p2-r*a by EUCLID:52;
  |[p`1-x, p2-r*a]|`1 = p`1-x by EUCLID:52;
  then |.|[p`1-x, p2-r*a]|.|^2 > (r*a)^2 by A14,A17,JGRAPH_1:29;
  then |.p-|[x,r*a]|.|^2 > (r*a)^2 by A2,EUCLID:62;
  then
A18: |.p-|[x,r*a]|.| > r*a by SQUARE_1:48;
A19: r*b-|.p-|[x,r*b]|.|+|.p-|[x,r*b]|.| = r*b;
  set r1 = min(r*b-|.p-|[x,r*b]|.|, |.p-|[x,r*a]|.|-r*a);
A20: |.p-|[x,r*b]|.| = |.|[x,r*b]|-p.| by TOPRNS_1:27;
  |[p`1-x, p2-r*b]|`1 = p`1-x by EUCLID:52;
  then |.|[p`1-x, p2-r*b]|.|^2 < (r*b)^2 by A15,A16,JGRAPH_1:29;
  then
A21: |.p-|[x,r*b]|.|^2 < (r*b)^2 by A2,EUCLID:62;
  r*b9 >= 0;
  then |.p-|[x,r*b]|.| < r*b by A21,SQUARE_1:48;
  then
  r*b-|.p-|[x,r*b]|.| > 0 & r1 = r*b-|.p-|[x,r*b]|.| or |.p-|[x,r*a]|.|-r
  *a > 0 & r1 = |.p-|[x,r*a]|.|-r*a by A18,XREAL_1:50,XXREAL_0:15;
  then reconsider r1 as positive Real;
  take r1;
  r1 <= r*b-|.p-|[x,r*b]|.| by XXREAL_0:17;
  then
A22: |.|[x,r*b]|-p.|+r1 <= r*b by A20,A19,XREAL_1:6;
  |.p-|[p`1,0]|.| = |.|[p`1-p`1,p2-0]|.| by A2,EUCLID:62
    .= |.p2.| by TOPREAL6:23
    .= p2 by ABSVALUE:def 1;
  then
A23: |.|[x,r*b]|-|[p`1,0]|.| <= |.|[x,r*b]|-p.|+p2 by TOPRNS_1:34;
  thus now
    assume r1 > p`2;
    then |.|[x,r*b]|-p.|+p2 < |.|[x,r*b]|-p.|+r1 by XREAL_1:8;
    then |.|[x,r*b]|-|[p`1,0]|.| < |.|[x,r*b]|-p.|+r1 by A23,XXREAL_0:2;
    then |.|[x,r*b]|-|[p`1,0]|.| < r*b by A22,XXREAL_0:2;
    then |.|[p`1,0]|-|[x,r*b]|.| < r*b by TOPRNS_1:27;
    then
A24: |[p`1,0]| in Ball(|[x,r*b]|,r*b) by TOPREAL9:7;
    |[p`1,0]| in y=0-line;
    then Ball(|[x,r*b]|,r*b9) meets y=0-line by A24,XBOOLE_0:3;
    hence contradiction by Th21;
  end;
  then
A25: Ball(p,r1) c= y>=0-plane by A2,Th20;
  let u be object;
  assume
A26: u in Ball(p,r1);
  then reconsider q = u as Point of TOP-REAL 2;
A27: |.q-p.| < r1 by A26,TOPREAL9:7;
  then |.q-p.|+|.p-|[x,r*b]|.| < r1+|.p-|[x,r*b]|.| by XREAL_1:8;
  then
A28: |.q-p.|+|.p-|[x,r*b]|.| < r*b by A20,A22,XXREAL_0:2;
  |.q-|[x,r*b]|.| <= |.q-p.|+|.p-|[x,r*b]|.| by TOPRNS_1:34;
  then |.q-|[x,r*b]|.| < r*b by A28,XXREAL_0:2;
  then
A29: +(x,r).q < b by A6,Th63;
A30: |.p-|[x,r*a]|.| <= |.p-q.|+|.q-|[x,r*a]|.| by TOPRNS_1:34;
  a < b by A8,A9,XXREAL_0:2;
  then
A31: a < 1 by A6,XXREAL_0:2;
  |.p-|[x,r*a]|.|-r*a >= r1 by XXREAL_0:17;
  then |.p-|[x,r*a]|.|-r*a > |.q-p.| by A27,XXREAL_0:2;
  then
A32: |.p-|[x,r*a]|.|-|.q-p.| > r*a by XREAL_1:12;
  |.p-q.| = |.q-p.| by TOPRNS_1:27;
  then |.q-|[x,r*a]|.| >= |.p-|[x,r*a]|.|-|.q-p.| by A30,XREAL_1:20;
  then
A33: |.q-|[x,r*a]|.| > r*a by A32,XXREAL_0:2;
  q = |[q`1,q`2]| by EUCLID:53;
  then q`2 >= 0 by A25,A26,Th18;
  then +(x,r).q > a by A33,A5,A31,Th64;
  then +(x,r).q in ].a,b.[ by A29,XXREAL_1:4;
  hence thesis by A25,A26,Lm1,FUNCT_2:38;
end;

theorem Th66:
  for x being Real, a,r being positive Real holds
  Ball(|[x,r*a]|,r*a) c= +(x,r)"].0,a.[
proof
  let x be Real;
  let a,r be positive Real, u be object;
  assume
A1: u in Ball(|[x,r*a]|,r*a);
  then reconsider p = u as Point of TOP-REAL 2;
  Ball(|[x,r*a]|,r*a) c= y>=0-plane by Th20;
  then reconsider q = p as Point of Niemytzki-plane by A1,Def3;
  q = |[p`1,p`2]| by EUCLID:53;
  then
A2: p`2 >= 0 by Lm1,Th18;
A3: now
    assume +(x,r).p = 0;
    then p = |[x,0]| by A2,Th60;
    then
A4: p in y=0-line;
    Ball(|[x,r*a]|,r*a) misses y=0-line by Th21;
    hence contradiction by A4,A1,XBOOLE_0:3;
  end;
A5: +(x,r).q <= 1 by BORSUK_1:40,XXREAL_1:1;
  per cases;
  suppose
A6: a > 1;
A7: +(x,r).q > 0 by A3,BORSUK_1:40,XXREAL_1:1;
    +(x,r).q < a by A6,A5,XXREAL_0:2;
    then +(x,r).q in ].0,a.[ by A7,XXREAL_1:4;
    hence thesis by FUNCT_2:38;
  end;
  suppose
A8: a <= 1;
    |.p-|[x,r*a]|.| < r*a by A1,TOPREAL9:7;
    then
A9: +(x,r).p < a by A8,Th63;
    +(x,r).q > 0 by A3,BORSUK_1:40,XXREAL_1:1;
    then +(x,r).q in ].0,a.[ by A9,XXREAL_1:4;
    hence thesis by FUNCT_2:38;
  end;
end;

theorem Th67:
  for x being Real, a,r being positive Real holds
  Ball(|[x,r*a]|,r*a) \/ {|[x,0]|} c= +(x,r)"[.0,a.[
proof
  let x be Real;
  let a,r be positive Real, u be object;
  assume
A1: u in Ball(|[x,r*a]|,r*a) \/ {|[x,0]|};
  then
A2: u in Ball(|[x,r*a]|,r*a) or u in {|[x,0]|} by XBOOLE_0:def 3;
  reconsider p = u as Point of TOP-REAL 2 by A1;
A3: |[x,0]| in y>=0-plane;
  Ball(|[x,r*a]|,r*a) c= y>=0-plane by Th20;
  then reconsider q = p as Point of Niemytzki-plane by A3,A2,Lm1,TARSKI:def 1;
A4: +(x,r).q <= 1 by BORSUK_1:40,XXREAL_1:1;
A5: +(x,r).q >= 0 by BORSUK_1:40,XXREAL_1:1;
  per cases by A2,TARSKI:def 1;
  suppose
    a > 1;
    then +(x,r).q < a by A4,XXREAL_0:2;
    then +(x,r).q in [.0,a.[ by A5,XXREAL_1:3;
    hence thesis by FUNCT_2:38;
  end;
  suppose
A6: a <= 1 & u in Ball(|[x,r*a]|,r*a);
    then |.p-|[x,r*a]|.| < r*a by TOPREAL9:7;
    then +(x,r).p < a by A6,Th63;
    then +(x,r).q in [.0,a.[ by A5,XXREAL_1:3;
    hence thesis by FUNCT_2:38;
  end;
  suppose
    u = |[x,0]|;
    then +(x,r).u = 0 by Def5;
    then +(x,r).q in [.0,a.[ by XXREAL_1:3;
    hence thesis by FUNCT_2:38;
  end;
end;

theorem Th68:
  for p being Point of TOP-REAL 2 st p`2 >= 0 for x,a being Real
, r being positive Real st 0 < +(x,r).p & +(x,r).p < a & a <= 1
  holds p in Ball(|[x,r*a]|,r*a)
proof
  let p be Point of TOP-REAL 2;
  assume
A1: p`2 >= 0;
  let x,a be Real;
A2: p = |[p`1,p`2]| by EUCLID:53;
  let r be positive Real;
  set r1 = r*a;
  assume that
A3: 0 < +(x,r).p and
A4: +(x,r).p < a and
A5: a <= 1;
A6: x <> p`1 implies p <> |[p`1,0]| by A4,A5,Th61;
A7: p <> |[x,0]| by A3,Def5;
  assume not p in Ball(|[x,r1]|,r1);
  then |.p-|[x,r1]|.| >= r1 by TOPREAL9:7;
  then |.p-|[x,r1]|.| = r1 or |.p-|[x,r1]|.| > r1 & (a < 1 or a = 1) by A5,
XXREAL_0:1;
  then
  +(x,r).p = a or a < 1 & +(x,r).p > a or a = 1 & not p in Ball(|[x,r]|,r
  ) by A1,A2,A3,A5,A7,A6,Th62,Th64,TOPREAL9:7;
  hence thesis by A1,A2,A4,A7,A6,Def5;
end;

theorem Th69:
  for p being Point of TOP-REAL 2 st p`2 > 0 for x,a being Real
, r being positive Real st 0 <= a & a < +(x,r).p ex r1 being
  positive Real st r1 <= p`2 & Ball(p,r1) c= +(x,r)"].a,1.]
proof
  let p be Point of TOP-REAL 2;
  assume
A1: p`2 > 0;
  let x,a be Real;
  let r be positive Real;
  set f = +(x,r);
  assume that
A2: 0 <= a and
A3: a < f.p;
A4: p = |[p`1,p`2]| by EUCLID:53;
  then p in the carrier of Niemytzki-plane by A1,Lm1;
  then f.p in the carrier of I[01] by FUNCT_2:5;
  then f.p <= 1 by BORSUK_1:40,XXREAL_1:1;
  then
A5: a < 1 by A3,XXREAL_0:2;
  per cases by A2;
  suppose
A6: a = 0;
    reconsider r1 = p`2 as positive Real by A1;
    reconsider A = Ball(p,r1) as Subset of Niemytzki-plane by A4,Lm1,Th20;
    take r1;
    thus r1 <= p`2;
    let u be object;
    assume
A7: u in Ball(p,r1);
    then reconsider q = u as Point of TOP-REAL 2;
A8: q = |[q`1,q`2]| by EUCLID:53;
    q in A by A7;
    then
A9: q`2 >= 0 by A8,Lm1,Th18;
    q in A by A7;
    then reconsider z = q as Element of Niemytzki-plane;
A10: f.z >= 0 by BORSUK_1:40,XXREAL_1:1;
    y=0-line misses Ball(p,r1) by A4,Th21;
    then not q in y=0-line by A7,XBOOLE_0:3;
    then
A11: q`2 <> 0 by A8;
A12: f.z <= 1 by BORSUK_1:40,XXREAL_1:1;
    |[x,0]|`2 = 0 by EUCLID:52;
    then f.q <> 0 by A11,A9,Th60;
    then f.z in ].a,1.] by A10,A12,A6,XXREAL_1:2;
    hence thesis by FUNCT_2:38;
  end;
  suppose
    a > 0;
    then reconsider b = a as positive Real;
    set r1 = min(|.p-|[x,r*a]|.|-r*a, p`2);
A13: r1 = |.p-|[x,r*a]|.|-r*a or r1 = p`2 by XXREAL_0:def 9;
A14: b <> f.p by A3;
    not |.p-|[x,r*a]|.| < r*a by A3,A5,Th63;
    then |.p-|[x,r*a]|.| > r*a by A14,A1,A5,Th62,XXREAL_0:1;
    then reconsider r1 as positive Real by A13,A1,XREAL_1:50;
    take r1;
    thus r1 <= p`2 by XXREAL_0:17;
    then reconsider A = Ball(p,r1) as Subset of Niemytzki-plane by A4,Lm1,Th20;
    let u be object;
    assume
A15: u in Ball(p,r1);
    then reconsider q = u as Point of TOP-REAL 2;
    u in A by A15;
    then reconsider z = q as Point of Niemytzki-plane;
A16: q = |[q`1,q`2]| by EUCLID:53;
    q in A by A15;
    then
A17: q`2 >= 0 by A16,Lm1,Th18;
A18: now
      |.p-|[x,r*a]|.|-r*a >= r1 by XXREAL_0:17;
      then
A19:  r*a+r1 <= |.p-|[x,r*a]|.|-r*a+r*a by XREAL_1:6;
      assume not f.z > a;
      then |.q-|[x,r*a]|.| <= r*a by A2,A5,A17,Th64;
      then
A20:  |.|[x,r*a]|-q.| <= r*a by TOPRNS_1:27;
A21:  |.|[x,r*a]|-q.|+|.q-p.| >= |.|[x,r*a]|-p.| by TOPRNS_1:34;
      |.q-p.| < r1 by A15,TOPREAL9:7;
      then |.|[x,r*a]|-q.|+|.q-p.| < r*a+r1 by A20,XREAL_1:8;
      then |.|[x,r*a]|-p.| < r*a+r1 by A21,XXREAL_0:2;
      hence contradiction by A19,TOPRNS_1:27;
    end;
    f.z <= 1 by BORSUK_1:40,XXREAL_1:1;
    then f.z in ].a,1.] by A18,XXREAL_1:2;
    hence thesis by FUNCT_2:38;
  end;
end;

theorem Th70:
  for p being Point of TOP-REAL 2 st p`2 = 0 for x being Real
, r being positive Real st +(x,r).p = 1 ex r1 being positive
  Real st Ball(|[p`1,r1]|,r1) \/ {p} c= +(x,r)"{1}
proof
  let p be Point of TOP-REAL 2;
  assume
A1: p`2 = 0;
  let x be Real;
  let r be positive Real;
  set r1 = (|.p-|[x,r]|.|-r)/2;
  set f = +(x,r);
A2: p =|[p`1,p`2]| by EUCLID:53;
  assume
A3: f.p = 1;
  then p`1-x <> 0 by A2,A1,Def5;
  then (p`1-x)^2 > 0 by SQUARE_1:12;
  then (p`1-x)^2+(0-r)^2 > 0+(0-r)^2 by XREAL_1:6;
  then |.|[p`1-x,p`2-r]|.|^2 > r^2 by A1,Th9;
  then |.p-|[x,r]|.|^2 > r^2 by A2,EUCLID:62;
  then |.p-|[x,r]|.| > r by SQUARE_1:15;
  then |.p-|[x,r]|.|-r > 0 by XREAL_1:50;
  then reconsider r1 as positive Real;
  take r1;
  let u be object;
  assume
A4: u in Ball(|[p`1,r1]|,r1) \/ {p};
  then reconsider q = u as Point of TOP-REAL 2;
A5: Ball(|[p`1,r1]|,r1) c= y>=0-plane by Th20;
  u in Ball(|[p`1,r1]|,r1) or u = p by A4,ZFMISC_1:136;
  then reconsider z = q as Point of Niemytzki-plane by A5,A1,A2,Lm1,Th18;
A6: q = |[q`1,q`2]| by EUCLID:53;
A7: now
    assume
A8: q in Ball(|[p`1,r1]|,r1);
    then |.q-|[p`1,r1]|.| < r1 by TOPREAL9:7;
    then
A9: |.q-|[p`1,r1]|.|+|.|[p`1,r1]|-p.| < r1+|.|[p`1,r1]|-p.| by XREAL_1:6;
A10: |.r1.| = r1 by ABSVALUE:def 1;
A11: |.q-|[p`1,r1]|.|+|.|[p`1,r1]|-p.| >= |.q-p.| by TOPRNS_1:34;
A12: |.q-p.|+|.|[x,r]|-q.| >= |.|[x,r]|-p.| by TOPRNS_1:34;
A13: |.|[0,r1]|.| = |.r1.| by TOPREAL6:23;
    |[p`1,r1]|-p = |[p`1-p`1,r1-0]| by A1,A2,EUCLID:62;
    then r1+r1 > |.q-p.| by A9,A11,A10,A13,XXREAL_0:2;
    then |.p-|[x,r]|.|-r+|.|[x,r]|-q.| > |.q-p.|+|.|[x,r]|-q.| by XREAL_1:6;
    then |.|[x,r]|-p.| < |.p-|[x,r]|.|-r+|.|[x,r]|-q.| by A12,XXREAL_0:2;
    then
A14: |.|[x,r]|-p.|-(|.p-|[x,r]|.|-r) < |.|[x,r]|-q.| by XREAL_1:19;
    |.p-|[x,r]|.| = |.|[x,r]|-p.| by TOPRNS_1:27;
    then |.q-|[x,r]|.| > r by A14,TOPRNS_1:27;
    hence not q in Ball(|[x,r]|,r) by TOPREAL9:7;
    q`2 = 0 implies q in y=0-line & Ball(|[p`1,r1]|,r1) misses y=0-line
    by A6,Th21;
    hence q`2 <> 0 by A8,XBOOLE_0:3;
  end;
  z in y>=0-plane by Lm1;
  then q`2 >= 0 by A6,Th18;
  then f.z = 1 by A7,A3,A4,A6,Def5,ZFMISC_1:136;
  then f.z in {1} by TARSKI:def 1;
  hence thesis by FUNCT_2:38;
end;

theorem Th71:
  for T being non empty TopSpace, S being SubSpace of T for B
being Basis of T holds {A/\[#]S where A is Subset of T: A in B & A meets [#]S}
  is Basis of S
proof
  let T be non empty TopSpace;
  let S be SubSpace of T;
  let B be Basis of T;
  set X = {A/\[#]S where A is Subset of T: A in B & A meets [#]S};
  X c= bool the carrier of S
  proof
    let u be object;
    assume u in X;
    then ex A being Subset of T st u = A/\[#]S & A in B & A meets [#]S;
    hence thesis;
  end;
  then reconsider X as Subset-Family of S;
A1: now
    let U be Subset of S;
    assume U is open;
    then consider U0 being Subset of T such that
A2: U0 is open and
A3: U = U0 /\ the carrier of S by TSP_1:def 1;
    let x be Point of S;
    assume
A4: x in U;
    then x in U0 by A3,XBOOLE_0:def 4;
    then consider V0 being Subset of T such that
A5: V0 in B and
A6: x in V0 and
A7: V0 c= U0 by A2,YELLOW_9:31;
    reconsider V = V0 /\ [#]S as Subset of S;
    take V;
    V0 meets [#]S by A4,A6,XBOOLE_0:3;
    hence V in X by A5;
    thus x in V by A4,A6,XBOOLE_0:def 4;
    thus V c= U by A3,A7,XBOOLE_1:26;
  end;
  X c= the topology of S
  proof
    let u be object;
    assume u in X;
    then
A8: ex A being Subset of T st u = A/\[#]S & A in B & A meets [#]S;
    B c= the topology of T by TOPS_2:64;
    hence thesis by A8,PRE_TOPC:def 4;
  end;
  hence thesis by A1,YELLOW_9:32;
end;

theorem Th72:
  {].a,b.[ where a,b is Real: a < b} is Basis of R^1
proof
  set X = {].a,b.[ where a,b is Real: a < b};
  X c= bool REAL
  proof
    let u be object;
    assume u in X;
    then ex a,b being Real st u = ].a,b.[ & a < b;
    hence thesis;
  end;
  then reconsider X as Subset-Family of R^1 by TOPMETR:17;
A1: now
    let U be Subset of R^1 such that
A2: U is open;
    let x be Point of R^1 such that
A3: x in U;
    reconsider a = x as Real;
    consider r being Real such that
A4: 0 < r and
A5: ].a-r,a+r.[ c= U by A2,A3,FRECHET:8;
    reconsider V = ].a-r,a+r.[ as Subset of R^1 by TOPMETR:17;
    take V;
A6: a < a+r by A4,XREAL_1:29;
A7: a-r < a by A4,XREAL_1:44;
    then a-r < a+r by A6,XXREAL_0:2;
    hence V in X;
    thus x in V by A7,A6,XXREAL_1:4;
    thus V c= U by A5;
  end;
  X c= the topology of R^1
  proof
    let u be object;
    assume u in X;
    then ex a, b being Real st u = ].a,b.[ & a < b;
    then u is open Subset of R^1 by JORDAN6:35,TOPMETR:17;
    hence thesis by PRE_TOPC:def 2;
  end;
  hence thesis by A1,YELLOW_9:32;
end;

theorem Th73:
  for T being TopSpace for U,V being Subset of T for B being set
  st U in B & V in B & B \/ {U \/ V} is Basis of T holds B is Basis of T
proof
  let T be TopSpace;
  let U,V be Subset of T;
  let B be set;
  assume that
A1: U in B and
A2: V in B and
A3: B \/ {U \/ V} is Basis of T;
A4: B c= B \/ {U \/ V} by XBOOLE_1:7;
  then reconsider B9 = B as Subset-Family of T by A3,XBOOLE_1:1;
A5: now
A6: V c= U\/V by XBOOLE_1:7;
A7: U c= U\/V by XBOOLE_1:7;
    let A be Subset of T such that
A8: A is open;
    let p be Point of T;
    assume p in A;
    then consider A9 being Subset of T such that
A9: A9 in B \/ {U\/V} and
A10: p in A9 and
A11: A9 c= A by A3,A8,YELLOW_9:31;
    assume
A12: not ex a being Subset of T st a in B9 & p in a & a c= A;
    A9 in B or A9 = U \/ V by A9,ZFMISC_1:136;
    then p in U & U c= A or p in V & V c= A by A10,A11,A12,A7,A6,XBOOLE_0:def 3
;
    hence contradiction by A1,A2,A12;
  end;
  B \/ {U \/ V} c= the topology of T by A3,TOPS_2:64;
  hence thesis by A5,A4,XBOOLE_1:1,YELLOW_9:32;
end;

theorem Th74:
  {[.0,a.[ where a is Real: 0 < a & a <= 1} \/ {].a,1.] where a is
  Real: 0 <= a & a < 1} \/
   {].a,b.[ where a,b is Real: 0 <= a & a < b & b <= 1}
  is Basis of I[01]
proof
  reconsider U = [.0,2/3.[, V = ].1/3,1.] as Subset of I[01] by BORSUK_1:40
,XXREAL_1:35,36;
  reconsider B = {].a,b.[ where a,b is Real:
   a < b} as Basis of R^1 by Th72;
  set S = I[01], T = R^1;
  set A1 = {[.0,a.[ where a is Real: 0 < a & a <= 1};
  set A2 = {].a,1.] where a is Real: 0 <= a & a < 1};
  set A3 = {].a,b.[ where a,b is Real: 0 <= a & a < b & b <= 1};
  set B9 = {A/\[#]S where A is Subset of T: A in B & A meets [#]S};
A1: B9 = A1 \/ A2 \/ A3 \/ {[#]S}
  proof
    reconsider aa = ].-1,2.[ as Subset of T by TOPMETR:17;
    thus B9 c= A1 \/ A2 \/ A3 \/ {[#]S}
    proof
      let u be object;
      assume u in B9;
      then consider A being Subset of T such that
A2:   u = A/\[#]S and
A3:   A in B and
A4:   A meets [#]S;
      consider x being object such that
A5:   x in A and
A6:   x in [#]S by A4,XBOOLE_0:3;
      consider a,b being Real such that
A7:   A = ].a,b.[ and
A8:   a < b by A3;
      reconsider x as Real by A5;
A9:   a < x by A7,A5,XXREAL_1:4;
A10:  x <= 1 by A6,BORSUK_1:40,XXREAL_1:1;
A11:  0 <= x by A6,BORSUK_1:40,XXREAL_1:1;
      per cases;
      suppose
A12:    a < 0 & b <= 1;
A13:    0 < b by A11,A7,A5,XXREAL_1:4;
        u = [.0,b.[ by A12,A2,A7,BORSUK_1:40,XXREAL_1:148;
        then u in A1 by A13,A12;
        then u in A1 \/ A2 by XBOOLE_0:def 3;
        then u in A1 \/ A2 \/ (A3 \/ {[#]S}) by XBOOLE_0:def 3;
        hence thesis by XBOOLE_1:4;
      end;
      suppose
        a < 0 & b > 1;
        then u = [#]S by A2,A7,BORSUK_1:40,XBOOLE_1:28,XXREAL_1:47;
        hence thesis by ZFMISC_1:136;
      end;
      suppose
A14:    a >= 0 & b <= 1;
        then u = A by A2,A7,BORSUK_1:40,XBOOLE_1:28,XXREAL_1:37;
        then u in A3 by A7,A8,A14;
        then u in A1 \/ A2 \/ A3 by XBOOLE_0:def 3;
        hence thesis by XBOOLE_0:def 3;
      end;
      suppose
A15:    a >= 0 & b > 1;
A16:    a < 1 by A10,A9,XXREAL_0:2;
        u = ].a,1.] by A15,A2,A7,BORSUK_1:40,XXREAL_1:149;
        then u in A2 by A16,A15;
        then u in A1 \/ A2 by XBOOLE_0:def 3;
        then u in A1 \/ A2 \/ (A3 \/ {[#]S}) by XBOOLE_0:def 3;
        hence thesis by XBOOLE_1:4;
      end;
    end;
    let u be object;
    assume u in A1 \/ A2 \/ A3 \/ {[#]S};
    then u in A1 \/ A2 \/ A3 or u in {[#]S} by XBOOLE_0:def 3;
    then
A17: u in A1 \/ A2 or u in A3 or u in {[#]S} by XBOOLE_0:def 3;
    per cases by A17,XBOOLE_0:def 3;
    suppose
      u in {[#]S};
      then u = [#]S by TARSKI:def 1;
      then
A18:  u = aa/\[#]S by BORSUK_1:40,XBOOLE_1:28,XXREAL_1:47;
      [#]S c= aa by BORSUK_1:40,XXREAL_1:47;
      then
A19:  aa meets [#]S by XBOOLE_1:68;
      aa in B;
      hence thesis by A18,A19;
    end;
    suppose
      u in A1;
      then consider a being Real such that
A20:  u = [.0,a.[ and
A21:  0 < a and
A22:  a <= 1;
      reconsider A = ].-1,a.[ as Subset of T by TOPMETR:17;
A23:  A in B by A21;
A24:  0 in [.0,1.] by XXREAL_1:1;
      0 in A by A21,XXREAL_1:4;
      then
A25:  A meets [#]S by A24,BORSUK_1:40,XBOOLE_0:3;
      u = A /\ [.0,1.] by A20,A22,XXREAL_1:148;
      hence thesis by A23,A25,BORSUK_1:40;
    end;
    suppose
      u in A2;
      then consider a being Real such that
A26:  u = ].a,1.] and
A27:  0 <= a and
A28:  a < 1;
      reconsider A = ].a,2.[ as Subset of T by TOPMETR:17;
      2 > a by A28,XXREAL_0:2;
      then
A29:  A in B;
A30:  1 in [.0,1.] by XXREAL_1:1;
      1 in A by A28,XXREAL_1:4;
      then
A31:  A meets [#]S by A30,BORSUK_1:40,XBOOLE_0:3;
      u = A /\ [.0,1.] by A26,A27,XXREAL_1:149;
      hence thesis by A29,A31,BORSUK_1:40;
    end;
    suppose
      u in A3;
      then consider a,b being Real such that
A32:  u = ].a,b.[ and
A33:  0 <= a and
A34:  a < b and
A35:  b <= 1;
      reconsider A = ].a,b.[ as Subset of T by TOPMETR:17;
A36:  A c= [.0,1.] by A33,A35,XXREAL_1:37;
      a+b < b+b by A34,XREAL_1:8;
      then
A37:  (a+b)/2 < (b+b)/2 by XREAL_1:74;
      a+a < a+b by A34,XREAL_1:8;
      then (a+a)/2 < (a+b)/2 by XREAL_1:74;
      then (a+b)/2 in A by A37,XXREAL_1:4;
      then
A38:  A meets [#]S by A36,BORSUK_1:40,XBOOLE_0:3;
A39:  A in B by A34;
      u = A /\ [.0,1.] by A33,A35,A32,XBOOLE_1:28,XXREAL_1:37;
      hence thesis by A39,A38,BORSUK_1:40;
    end;
  end;
  U in A1;
  then U in A1 \/ A2 by XBOOLE_0:def 3;
  then
A40: U in A1 \/ A2 \/ A3 by XBOOLE_0:def 3;
  V in A2;
  then V in A1 \/ A2 by XBOOLE_0:def 3;
  then
A41: V in A1 \/ A2 \/ A3 by XBOOLE_0:def 3;
  U \/ V = [#]S by BORSUK_1:40,XXREAL_1:175;
  hence thesis by A1,A40,A41,Th71,Th73;
end;

theorem Th75:
  for T being non empty TopSpace for f being Function of T, I[01]
holds f is continuous iff for a,b being Real st 0 <= a & a < 1 & 0 < b &
  b <= 1 holds f"[.0,b.[ is open & f"].a,1.] is open
proof
  set A3 = {].a,b.[ where a,b is Real: 0 <= a & a < b & b <= 1};
  set A2 = {].a,1.] where a is Real: 0 <= a & a < 1};
  set A1 = {[.0,a.[ where a is Real: 0 < a & a <= 1};
  reconsider B = A1 \/ A2 \/ A3 as Basis of I[01] by Th74;
  let T be non empty TopSpace;
  let f be Function of T, I[01];
  hereby
    assume
A1: f is continuous;
    let a,b be Real;
    reconsider x = a, y = b as Real;
    assume that
A2: 0 <= a and
A3: a < 1 and
A4: 0 < b and
A5: b <= 1;
    ].x,1.] in A2 by A2,A3;
    then ].x,1.] in A1 \/ A2 by XBOOLE_0:def 3;
    then
A6: ].x,1.] in B by XBOOLE_0:def 3;
    [.0,y.[ in A1 by A4,A5;
    then [.0,y.[ in A1 \/ A2 by XBOOLE_0:def 3;
    then [.0,y.[ in B by XBOOLE_0:def 3;
    hence f"[.0,b.[ is open & f"].a,1.] is open by A6,A1,YELLOW_9:34;
  end;
  assume
A7: for a,b being Real st 0 <= a & a < 1 & 0 < b & b <= 1 holds
  f"[.0,b.[ is open & f"].a,1.] is open;
  now
    let A be Subset of I[01];
    assume A in B;
    then
A8: A in A1 \/ A2 or A in A3 by XBOOLE_0:def 3;
    per cases by A8,XBOOLE_0:def 3;
    suppose
      A in A1;
      then ex a being Real st A = [.0,a.[ & 0 < a & a <= 1;
      hence f"A is open by A7;
    end;
    suppose
      A in A2;
      then ex a being Real st A = ].a,1.] & 0 <= a & a < 1;
      hence f"A is open by A7;
    end;
    suppose
      A in A3;
      then consider a,b being Real such that
A9:   A = ].a,b.[ and
A10:  0 <= a and
A11:  a < b and
A12:  b <= 1;
      a < 1 by A11,A12,XXREAL_0:2;
      then reconsider
      U = f"[.0,b.[, V = f"].a,1.] as open Subset of T by A10,A11,A7,A12;
      A = [.0,b.[ /\ ].a,1.] by A9,A10,A12,XXREAL_1:153;
      then f"A = U /\ V by FUNCT_1:68;
      hence f"A is open;
    end;
  end;
  hence thesis by YELLOW_9:34;
end;

registration
  let x be Real, r be positive Real;
  cluster +(x,r) -> continuous;
  coherence
  proof
    set f = +(x,r);
    consider BB being Neighborhood_System of Niemytzki-plane such that
A1: for x holds BB.(|[x,0]|) = {Ball(|[x,q]|,q) \/ {|[x,0]|} where q
    is Real: q > 0} and
A2: for x,y st y > 0 holds BB.(|[x,y]|) = {Ball(|[x,y]|,q) /\
    y>=0-plane where q is Real: q > 0} by Def3;
A3: dom BB = y>=0-plane by Lm1,PARTFUN1:def 2;
    now
      let a,b be Real;
      assume that
A4:   0 <= a and
A5:   a < 1 and
A6:   0 < b and
A7:   b <= 1;
      now
        let c be Element of Niemytzki-plane;
        assume c in f"[.0,b.[;
        then
A8:     f.c in [.0,b.[ by FUNCT_1:def 7;
        c in y>=0-plane by Lm1;
        then reconsider z = c as Point of TOP-REAL 2;
        z = |[z`1,z`2]| by EUCLID:53;
        then
A9:     z`2 >= 0 by Lm1,Th18;
        per cases by A8,XXREAL_1:3;
        suppose
A10:      f.c = 0;
          reconsider r1 = r*b as positive Real by A6;
          reconsider U = Ball(|[x,r1]|,r1) \/ {|[x,0]|} as Subset of
          Niemytzki-plane by Th27;
          take U;
A11:      |[x,0]| in y>=0-plane;
          U in {Ball(|[x,q]|,q) \/ {|[x,0]|} where q is Real:
          q > 0};
          then
A12:      U in BB.(|[x,0]|) by A1;
          z = |[x,0]| by A10,A9,Th60;
          hence U in Union BB & c in U & U c= f"[.0,b.[ by A12,A11,A3,A6,Th67,
CARD_5:2,ZFMISC_1:136;
        end;
        suppose
A13:      0 < f.c & f.c < b;
          reconsider r1 = r*b as positive Real by A6;
          reconsider U = Ball(|[x,r1]|,r1) as Subset of Niemytzki-plane by Th29
;
          take U;
A14:      |[x,r1]| in y>=0-plane;
          U c= y>=0-plane by Th20;
          then U /\ y>=0-plane = U by XBOOLE_1:28;
          then
          U in {Ball(|[x,r1]|,q) /\ y>=0-plane where q is Real
          : q > 0};
          then U in BB.(|[x,r1]|) by A2;
          hence U in Union BB by A14,A3,CARD_5:2;
A15:      f"].0,b.[ c= f"[.0,b.[ by RELAT_1:143,XXREAL_1:45;
          Ball(|[x,r*b]|,r*b) c= +(x, r)"].0,b.[ by A13,Th66;
          hence c in U & U c= f"[.0,b.[ by A15,A13,A7,A9,Th68;
        end;
      end;
      hence f"[.0,b.[ is open by YELLOW_9:31;
      now
        let c be Element of Niemytzki-plane;
        c in y>=0-plane by Lm1;
        then reconsider z = c as Point of TOP-REAL 2;
        assume c in f"].a,1.];
        then
A16:    f.c in ].a,1.] by FUNCT_1:def 7;
        then
A17:    f.c > a by XXREAL_1:2;
A18:    f.c <= 1 by A16,XXREAL_1:2;
A19:    z = |[z`1,z`2]| by EUCLID:53;
        then
A20:    z`2 >= 0 by Lm1,Th18;
        per cases by A19,A16,A18,Lm1,Th18,XXREAL_0:1,XXREAL_1:2;
        suppose
          z`2 > 0;
          then consider r1 being positive Real such that
A21:      r1 <= z`2 and
A22:      Ball(z,r1) c= +(x,r)"].a,1.] by A4,A17,Th69;
          reconsider U = Ball(z,r1) as Subset of Niemytzki-plane by A19,A21
,Th29;
          U c= y>=0-plane by A19,A21,Th20;
          then
A23:      U /\ y>=0-plane = U by XBOOLE_1:28;
          U in {Ball(|[z`1,z`2]|,q) /\ y>=0-plane
            where q is Real: q > 0} by A23,A19;
          then
A24:      U in BB.(|[z`1,z`2]|) by A21,A2;
          take U;
          |[z`1,z`2]| in y>=0-plane by A21;
          hence U in Union BB by A24,A3,CARD_5:2;
          thus c in U & U c= f"].a,1.] by A22,Th13;
        end;
        suppose
A25:      f.c = 1 & z`2 = 0;
          then consider r1 being positive Real such that
A26:      Ball(|[z`1,r1]|,r1) \/ {z} c= +(x,r)"{1} by Th70;
          reconsider U = Ball(|[z`1,r1]|,r1) \/ {z} as Subset of
          Niemytzki-plane by A19,A25,Th27;
          U in {Ball(|[z`1,q]|,q) \/ {|[z`1,0]|}
             where q is Real: q > 0} by A19,A25;
          then
A27:      U in BB.(|[z`1,z`2]|) by A1,A25;
          take U;
          |[z`1,z`2]| in y>=0-plane by A25;
          hence U in Union BB by A27,A3,CARD_5:2;
          thus c in U by ZFMISC_1:136;
          1 in ].a,1.] by A5,XXREAL_1:2;
          then {1} c= ].a,1.] by ZFMISC_1:31;
          then f"{1} c= f"].a,1.] by RELAT_1:143;
          hence U c= f"].a,1.] by A26;
        end;
        suppose
          a < f.c & f.c < 1;
          then f.c in ].a,1.[ by XXREAL_1:4;
          then consider r1 being positive Real such that
A28:      r1 <= z`2 and
A29:      Ball(z,r1) c= +(x,r)"].a,1.[ by A4,A20,Th65;
          reconsider U = Ball(z,r1) as Subset of Niemytzki-plane by A19,A28
,Th29;
          U c= y>=0-plane by A19,A28,Th20;
          then
A30:      U /\ y>=0-plane = U by XBOOLE_1:28;
          U in {Ball(|[z`1,z`2]|,q) /\ y>=0-plane
           where q is Real: q > 0} by A30,A19;
          then
A31:      U in BB.(|[z`1,z`2]|) by A28,A2;
          take U;
          |[z`1,z`2]| in y>=0-plane by A28;
          hence U in Union BB by A31,A3,CARD_5:2;
          f"].a,1.[ c= f"].a,1.] by RELAT_1:143,XXREAL_1:41;
          hence c in U & U c= f"].a,1.] by A29,Th13;
        end;
      end;
      hence f"].a,1.] is open by YELLOW_9:31;
    end;
    hence thesis by Th75;
  end;
end;

theorem Th76:
  for U being Subset of Niemytzki-plane for x,r st U = Ball(|[x,r
]|,r) \/ {|[x,0]|} ex f being continuous Function of Niemytzki-plane, I[01] st
f.(|[x,0]|) = 0 & for a,b being Real holds (|[a,b]| in U` implies f.(|[a
,b]|) = 1) & (|[a,b]| in U\{|[x,0]|} implies f.(|[a,b]|) = |.|[x,0]|-|[a,b]|.|
  ^2/(2*r*b))
proof
  let U be Subset of Niemytzki-plane;
  let x,r;
  assume
A1: U = Ball(|[x,r]|,r) \/ {|[x,0]|};
  take f = +(x,r);
  thus f.(|[x,0]|) = 0 by Def5;
  let a,b be Real;
  thus |[a,b]| in U` implies f.(|[a,b]|) = 1
  proof
    assume
A2: |[a,b]| in U`;
    then
A3: not |[a,b]| in U by XBOOLE_0:def 5;
    then
A4: not |[a,b]| in Ball(|[x,r]|,r) by A1,ZFMISC_1:136;
A5: a <> x or b <> 0 by A3,A1,ZFMISC_1:136;
    b >= 0 by A2,Lm1,Th18;
    hence thesis by A4,A5,Def5;
  end;
  assume
A6: |[a,b]| in U\{|[x,0]|};
  then
A7: not |[a,b]| in {|[x,0]|} by XBOOLE_0:def 5;
  |[a,b]| in U by A6,XBOOLE_0:def 5;
  then
A8: |[a,b]| in Ball(|[x,r]|,r) by A7,A1,XBOOLE_0:def 3;
  b >= 0 by A6,Lm1,Th18;
  hence thesis by A8,Def5;
end;

::<DESC name="1.4.5. Przyk/lad funkcji ci/ag/lej z p/laszczyzny Niemytzkiego w R^1" monograph="topology"/>

definition
  let x,y be Real, r be positive Real;
  func +(x,y,r) -> Function of Niemytzki-plane, I[01] means
  :Def6:
  for a being
Real, b being non negative Real holds (not |[a,b]| in Ball(|[x,
y]|,r) implies it.(|[a,b]|) = 1) & (|[a,b]| in Ball(|[x,y]|,r) implies it.(|[a,
  b]|) = |.|[x,y]|-|[a,b]|.|/r);
  existence
  proof
    deffunc F1(Point of TOP-REAL 2) = 1;
    deffunc F2(Point of TOP-REAL 2) = |.|[x,y]|-$1.|/r;
    defpred P[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 (P[a] implies F1(a) in the carrier of I[01]) & (not P[a] implies F2(a) in
    the carrier of I[01])
    proof
      let a be Point of TOP-REAL 2;
      assume a in the carrier of Niemytzki-plane;
      thus P[a] implies F1(a) in the carrier of I[01] by BORSUK_1:40,XXREAL_1:1
;
      assume not P[a];
      then |.a-|[x,y]|.| < r by TOPREAL9:7;
      then |.|[x,y]|-a.| < r by TOPRNS_1:27;
      then
A2:   F2(a) < r/r by XREAL_1:74;
      r/r = 1 by XCMPLX_1:60;
      hence thesis by A2,BORSUK_1:40,XXREAL_1:1;
    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 (P[a] implies f.a = F1(a)) & (not P[a] implies f.a = F2(a
    )) from SCH1(A3,A1);
    take f;
    let a be Real, b be non negative Real;
    |[a,b]| in the carrier of Niemytzki-plane by Lm1;
    hence thesis by A4;
  end;
  uniqueness
  proof
    let f,g be Function of Niemytzki-plane, I[01] such that
A5: for a being Real, 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) and
A6: for a being Real, b being non negative Real holds
(not |[a,b]| in Ball(|[x,y]|,r) implies g.(|[a,b]|) = 1) & (|[a,b]| in Ball(|[x
    ,y]|,r) implies g.(|[a,b]|) = |.|[x,y]|-|[a,b]|.|/r);
A7: the carrier of Niemytzki-plane = y>=0-plane by Def3;
    now
      let p be Point of Niemytzki-plane;
      p in y>=0-plane by A7;
      then reconsider q = p as Point of TOP-REAL 2;
A8:   p = |[q`1,q`2]| by EUCLID:53;
      then reconsider q2 = q`2 as non negative Real by A7,Th18;
      per cases;
      suppose
A9:     not |[q`1,q2]| in Ball(|[x,y]|,r);
        then f.p = 1 by A5,A8;
        hence f.p = g.p by A9,A6,A8;
      end;
      suppose
A10:    |[q`1,q2]| in Ball(|[x,y]|,r);
        then f.p = |.|[x,y]|-q.|/r by A5,A8;
        hence f.p = g.p by A10,A6,A8;
      end;
    end;
    hence thesis;
  end;
end;

theorem Th77:
  for p being Point of TOP-REAL 2 st p`2 >= 0 for x being Real
, y being non negative Real for r being positive Real
  holds +(x,y,r).p = 0 iff p = |[x,y]|
proof
  let p be Point of TOP-REAL 2;
  assume
A1: p`2 >= 0;
  let x be Real;
  let y be non negative Real;
  let r be positive Real;
A2: p = |[p`1,p`2]| by EUCLID:53;
  hereby
    assume
A3: +(x,y,r).p = 0;
    then p in Ball(|[x,y]|,r) by A1,A2,Def6;
    then 0 = |.|[x,y]|-p.|/r by A1,A2,A3,Def6;
    then 0 * r = |.|[x,y]|-p.|;
    hence p = |[x,y]| by TOPRNS_1:28;
  end;
  assume
A4: p = |[x,y]|;
  then p in Ball(|[x,y]|,r) by Th13;
  hence +(x,y,r).p = |.|[x,y]|-p.|/r by A4,Def6
    .= 0/r by A4,TOPRNS_1:28
    .= 0;
end;

theorem Th78:
  for x being Real, y being non negative Real for
r,a being positive Real st a <= 1 holds +(x,y,r)"[.0,a.[ = Ball(|[x,y
  ]|,r*a) /\ y>=0-plane
proof
  let x be Real;
  let y be non negative Real;
  let r,a be positive Real;
  set f = +(x,y,r);
  assume
A1: a <= 1;
  then r*a <= r*1 by XREAL_1:64;
  then
A2: Ball(|[x,y]|,r*a) c= Ball(|[x,y]|,r) by JORDAN:18;
  thus +(x,y,r)"[.0,a.[ c= Ball(|[x,y]|,r*a) /\ y>=0-plane
  proof
    let u be object;
    assume
A3: u in f"[.0,a.[;
    then reconsider p = u as Point of Niemytzki-plane;
    p in y>=0-plane by Lm1;
    then reconsider q = p as Element of TOP-REAL 2;
    f.p in [.0,a.[ by A3,FUNCT_2:38;
    then
A4: f.p < a by XXREAL_1:3;
A5: p = |[q`1,q`2]| by EUCLID:53;
    then
A6: q`2 >= 0 by Lm1,Th18;
    then p in Ball(|[x,y]|,r) by A4,A1,A5,Def6;
    then f.p = |.|[x,y]|-q.|/r by A5,A6,Def6;
    then
A7: |.|[x,y]|-q.| < r*a by A4,XREAL_1:77;
    |.|[x,y]|-q.| = |.q-|[x,y]|.| by TOPRNS_1:27;
    then p in Ball(|[x,y]|,r*a) by A7,TOPREAL9:7;
    hence thesis by Lm1,XBOOLE_0:def 4;
  end;
  let u be object;
  assume
A8: u in Ball(|[x,y]|,r*a) /\ y>=0-plane;
  then reconsider p = u as Point of Niemytzki-plane by Lm1,XBOOLE_0:def 4;
  reconsider q = p as Element of TOP-REAL 2 by A8;
A9: u in Ball(|[x,y]|,r*a) by A8,XBOOLE_0:def 4;
  then
A10: |.q-|[x,y]|.| < r*a by TOPREAL9:7;
A11: |.|[x,y]|-q.| = |.q-|[x,y]|.| by TOPRNS_1:27;
A12: p = |[q`1,q`2]| by EUCLID:53;
  u in y>=0-plane by A8,XBOOLE_0:def 4;
  then q`2 >= 0 by A12,Th18;
  then
A13: f.p = |.|[x,y]|-q.|/r by A2,A9,A12,Def6;
  then r*(f.p) = |.|[x,y]|-q.| by XCMPLX_1:87;
  then f.p < a by A10,A11,XREAL_1:64;
  then f.p in [.0,a.[ by A13,XXREAL_1:3;
  hence thesis by FUNCT_2:38;
end;

theorem Th79:
  for p being Point of TOP-REAL 2 st p`2 > 0 for x being Real
, a being non negative Real for y,r being positive Real
  st +(x,y,r).p > a holds |.|[x,y]|-p.| > r*a & Ball(p,|.|[x,y]|-p.|-r*a) /\
  y>=0-plane c= +(x,y,r)"].a,1.]
proof
  let p be Point of TOP-REAL 2;
  assume
A1: p`2 > 0;
  let x be Real;
  let a be non negative Real;
  let y,r be positive Real;
  set f = +(x,y,r);
A2: p = |[p`1,p`2]| by EUCLID:53;
  then p in y>=0-plane by A1;
  then f.p in [.0,1.] by Lm1,BORSUK_1:40,FUNCT_2:5;
  then
A3: f.p <= 1 by XXREAL_1:1;
  assume
A4: f.p > a;
  then
A5: a < 1 by A3,XXREAL_0:2;
A6: |.|[x,y]|-p.| = |.p-|[x,y]|.| by TOPRNS_1:27;
  thus |.|[x,y]|-p.| > r*a
  proof
    per cases by A3,XXREAL_0:1;
    suppose
      f.p < 1;
      then p in Ball(|[x,y]|,r) by A1,A2,Def6;
      then f.p = |.|[x,y]|-p.|/r by A1,A2,Def6;
      hence thesis by A4,XREAL_1:79;
    end;
    suppose
A7:   f.p = 1;
      now
A8:     r/r = 1 by XCMPLX_1:60;
        assume
A9:     p in Ball(|[x,y]|,r);
        then
A10:    |.p-|[x,y]|.| < r by TOPREAL9:7;
        1 = |.|[x,y]|-p.|/r by A9,A1,A2,A7,Def6;
        hence contradiction by A10,A8,A6,XREAL_1:74;
      end;
      then
A11:  |.p-|[x,y]|.| >= r by TOPREAL9:7;
      r*1 > r*a by A5,XREAL_1:68;
      hence thesis by A11,A6,XXREAL_0:2;
    end;
  end;
  then reconsider r1 = |.|[x,y]|-p.|-r*a as positive Real by XREAL_1:50;
  let u be object;
  assume
A12: u in Ball(p,|.|[x,y]|-p.|-r*a) /\ y>=0-plane;
  then reconsider z = u as Point of Niemytzki-plane by Lm1,XBOOLE_0:def 4;
  reconsider q = z as Element of TOP-REAL 2 by A12;
  u in Ball(p,|.|[x,y]|-p.|-r*a) by A12,XBOOLE_0:def 4;
  then |.q-p.| < r1 by TOPREAL9:7;
  then
A13: |.|[x,y]|-q.|+|.q-p.| < |.|[x,y]|-q.|+r1 by XREAL_1:6;
A14: q = |[q`1,q`2]| by EUCLID:53;
  then
A15: q`2 >= 0 by Lm1,Th18;
  |.|[x,y]|-p.| <= |.|[x,y]|-q.|+|.q-p.| by TOPRNS_1:34;
  then |.|[x,y]|-p.| < |.|[x,y]|-q.|+r1 by A13,XXREAL_0:2;
  then
A16: |.|[x,y]|-p.|-r1 < |.|[x,y]|-q.|+r1-r1 by XREAL_1:9;
A17: now
    assume q in Ball(|[x,y]|,r);
    then f.q = |.|[x,y]|-q.|/r by A14,A15,Def6;
    hence f.z > a by A16,XREAL_1:81;
  end;
  f.z in [.0,1.] by BORSUK_1:40;
  then
A18: f.z <= 1 by XXREAL_1:1;
  not q in Ball(|[x,y]|,r) implies f.q = 1 by A15,A14,Def6;
  then f.z in ].a,1.] by A18,A5,A17,XXREAL_1:2;
  hence thesis by FUNCT_2:38;
end;

theorem Th80:
  for p being Point of TOP-REAL 2 st p`2 = 0 for x being Real
, a being non negative Real for y,r being positive Real
st +(x,y,r).p > a holds |.|[x,y]|-p.| > r*a & ex r1 being positive Real
 st r1 = (|.|[x,y]|-p.|-r*a)/2 & Ball(|[p`1,r1]|,r1) \/ {p} c= +(x,y,r)"].a,1
  .]
proof
  let p be Point of TOP-REAL 2;
A1: p = |[p`1,p`2]| by EUCLID:53;
  assume
A2: p`2 = 0;
  then reconsider p9 = p as Point of Niemytzki-plane by A1,Lm1,Th18;
  let x be Real;
  let a be non negative Real;
  let y,r be positive Real;
  set f = +(x,y,r);
  p in y>=0-plane by A2,A1;
  then f.p in [.0,1.] by Lm1,BORSUK_1:40,FUNCT_2:5;
  then
A3: f.p <= 1 by XXREAL_1:1;
  assume
A4: f.p > a;
  then
A5: a < 1 by A3,XXREAL_0:2;
A6: |.|[x,y]|-p.| = |.p-|[x,y]|.| by TOPRNS_1:27;
  thus |.|[x,y]|-p.| > r*a
  proof
    per cases by A3,XXREAL_0:1;
    suppose
      f.p < 1;
      then p in Ball(|[x,y]|,r) by A2,A1,Def6;
      then f.p = |.|[x,y]|-p.|/r by A2,A1,Def6;
      hence thesis by A4,XREAL_1:79;
    end;
    suppose
A7:   f.p = 1;
      now
A8:     r/r = 1 by XCMPLX_1:60;
        assume
A9:     p in Ball(|[x,y]|,r);
        then
A10:    |.p-|[x,y]|.| < r by TOPREAL9:7;
        1 = |.|[x,y]|-p.|/r by A9,A2,A1,A7,Def6;
        hence contradiction by A10,A8,A6,XREAL_1:74;
      end;
      then
A11:  |.p-|[x,y]|.| >= r by TOPREAL9:7;
      r*1 > r*a by A5,XREAL_1:68;
      hence thesis by A11,A6,XXREAL_0:2;
    end;
  end;
  then reconsider r9 = |.|[x,y]|-p.|-r*a as positive Real by XREAL_1:50;
  take r1 = r9/2;
  thus r1 = (|.|[x,y]|-p.|-r*a)/2;
  let u be object;
A12: Ball(|[p`1,r1]|,r1) c= y>=0-plane by Th20;
  assume
A13: u in Ball(|[p`1,r1]|,r1) \/ {p};
  then u in Ball(|[p`1,r1]|,r1) or u = p9 by ZFMISC_1:136;
  then reconsider z = u as Point of Niemytzki-plane by A12,Def3;
  reconsider q = z as Element of TOP-REAL 2 by A13;
A14: q = |[q`1,q`2]| by EUCLID:53;
  then
A15: q`2 >= 0 by Lm1,Th18;
  then
A16: not q in Ball(|[x,y]|,r) implies f.q = 1 by A14,Def6;
  per cases by A13,ZFMISC_1:136;
  suppose
    u = p9;
    then f.z in ].a,1.] by A4,A3,XXREAL_1:2;
    hence thesis by FUNCT_2:38;
  end;
  suppose
    u in Ball(|[p`1,r1]|,r1);
    then |.q-|[p`1,r1]|.| < r1 by TOPREAL9:7;
    then
A17: |.q-|[p`1,r1]|.|+|.|[p`1,r1]|-p.| < r1+|.|[p`1,r1]|-p.| by XREAL_1:6;
    |.q-p.| <= |.q-|[p`1,r1]|.|+|.|[p`1,r1]|-p.| by TOPRNS_1:34;
    then
A18: |.q-p.| < r1+|.|[p`1,r1]|-p.| by A17,XXREAL_0:2;
     reconsider r1 as Real;
A19: |.|[0,r1]|.| = |.r1.| by TOPREAL6:23;
A20: |.|[x,y]|-p.| <= |.|[x,y]|-q.|+|.q-p.| by TOPRNS_1:34;
A21: |.r1.| = r1 by ABSVALUE:def 1;
    |.|[p`1,r1]|-p.| = |.|[p`1-p`1,r1-0 ]|.| by A2,A1,EUCLID:62;
    then |.|[x,y]|-q.|+|.q-p.| < |.|[x,y]|-q.|+(r1+r1)
     by A18,A19,A21,XREAL_1:6;
    then |.|[x,y]|-p.| < |.|[x,y]|-q.|+(r1+r1) by A20,XXREAL_0:2;
    then
A22: |.|[x,y]|-p.|-(r1+r1) < |.|[x,y]|-q.|+(r1+r1)-(r1+r1) by XREAL_1:9;
A23: now
      assume q in Ball(|[x,y]|,r);
      then f.q = |.|[x,y]|-q.|/r by A14,A15,Def6;
      hence f.z > a by A22,XREAL_1:81;
    end;
    f.z in [.0,1.] by BORSUK_1:40;
    then f.z <= 1 by XXREAL_1:1;
    then f.z in ].a,1.] by A5,A16,A23,XXREAL_1:2;
    hence thesis by FUNCT_2:38;
  end;
end;

registration
  let x be Real;
  let y,r be positive Real;
  cluster +(x,y,r) -> continuous;
  coherence
  proof
    set f = +(x,y,r);
    consider BB being Neighborhood_System of Niemytzki-plane such that
A1: for x holds BB.(|[x,0]|) = {Ball(|[x,q]|,q) \/ {|[x,0]|} where q
    is Real: q > 0} and
A2: for x,y st y > 0 holds BB.(|[x,y]|) = {Ball(|[x,y]|,q) /\
    y>=0-plane where q is Real: q > 0} by Def3;
A3: dom BB = y>=0-plane by Lm1,PARTFUN1:def 2;
    now
      let a,b be Real;
      assume that
A4:   0 <= a and
      a < 1 and
A5:   0 < b and
A6:   b <= 1;
      f"[.0,b.[ = Ball(|[x,y]|,r*b) /\ y>=0-plane by A5,A6,Th78;
      hence f"[.0,b.[ is open by A5,Th28;
      now
        let c be Element of Niemytzki-plane;
        c in y>=0-plane by Lm1;
        then reconsider z = c as Point of TOP-REAL 2;
A7:     z = |[z`1,z`2]| by EUCLID:53;
        assume c in f"].a,1.];
        then f.c in ].a,1.] by FUNCT_1:def 7;
        then
A8:     f.c > a by XXREAL_1:2;
        per cases by A7,Lm1,Th18;
        suppose
A9:       z`2 > 0;
          then reconsider r1 = |.|[x,y]|-z.|-r*a as positive Real by A4,A8,Th79
,XREAL_1:50;
          reconsider U = Ball(z,r1) /\ y>=0-plane as Subset of Niemytzki-plane
          by A7,A9,Th28;
          U in {Ball(|[z`1,z`2]|,q) /\ y>=0-plane
          where q is Real: q > 0} by A7;
          then
A10:      U in BB.(|[z`1,z`2]|) by A2,A9;
          take U;
          |[z`1,z`2]| in y>=0-plane by A9;
          hence U in Union BB by A10,A3,CARD_5:2;
          c in Ball(z,r1) by Th13;
          hence c in U & U c= f"].a,1.] by A4,A8,A9,Lm1,Th79,XBOOLE_0:def 4;
        end;
        suppose
A11:      z`2 = 0;
          then consider r1 being positive Real such that
          r1 = (|.|[x,y]|-z.|-r*a)/2 and
A12:      Ball(|[z`1,r1]|,r1) \/ {z} c= +(x,y,r)"].a,1.] by A4,A8,Th80;
          reconsider U = Ball(|[z`1,r1]|,r1) \/ {z} as Subset of
          Niemytzki-plane by A7,A11,Th27;
          U in {Ball(|[z`1,q]|,q) \/ {|[z`1,0]|}
            where q is Real: q > 0} by A7,A11;
          then
A13:      U in BB.(|[z`1,z`2]|) by A1,A11;
          take U;
          |[z`1,z`2]| in y>=0-plane by A11;
          hence U in Union BB by A13,A3,CARD_5:2;
          thus c in U by ZFMISC_1:136;
          thus U c= f"].a,1.] by A12;
        end;
      end;
      hence f"].a,1.] is open by YELLOW_9:31;
    end;
    hence thesis by Th75;
  end;
end;

theorem Th81:
  for U being Subset of Niemytzki-plane for x,y,r st y > 0 & U =
Ball(|[x,y]|,r) /\ y>=0-plane ex f being continuous Function of Niemytzki-plane
  , I[01] st f.(|[x,y]|) = 0 & for a,b being Real holds (|[a,b]| in U`
implies f.(|[a,b]|) = 1) & (|[a,b]| in U implies f.(|[a,b]|) = |.|[x,y]|-|[a,b
  ]|.|/r)
proof
  let U be Subset of Niemytzki-plane;
  let x,y,r;
  assume that
A1: y > 0 and
A2: U = Ball(|[x,y]|,r) /\ y>=0-plane;
  reconsider y9 = y as positive Real by A1;
  take f = +(x,y9,r);
  |[x,y9]|`2 = y by EUCLID:52;
  hence f.(|[x,y]|) = 0 by Th77;
  let a,b be Real;
  thus |[a,b]| in U` implies f.(|[a,b]|) = 1
  proof
    assume
A3: |[a,b]| in U`;
    then not |[a,b]| in U by XBOOLE_0:def 5;
    then
A4: not |[a,b]| in Ball(|[x,y]|,r) by A2,A3,Lm1,XBOOLE_0:def 4;
    b >= 0 by A3,Lm1,Th18;
    hence thesis by A4,Def6;
  end;
  assume
A5: |[a,b]| in U;
  then
A6: |[a,b]| in Ball(|[x,y]|,r) by A2,XBOOLE_0:def 4;
  b >= 0 by A5,Lm1,Th18;
  hence thesis by A6,Def6;
end;

theorem Th82:
  Niemytzki-plane is T_1
proof
  set X = Niemytzki-plane;
  let x,y be Point of X;
A1: the carrier of X = y>=0-plane by Def3;
  then
A2: y in y>=0-plane;
  x in y>=0-plane by A1;
  then reconsider a = x, b = y as Point of TOP-REAL 2 by A2;
  assume x <> y;
  then |.a-b.| <> 0 by TOPRNS_1:28;
  then reconsider r = |.a-b.| as positive Real;
  consider q being Point of TOP-REAL 2, U being open Subset of X such that
A3: x in U and
  q in U and
A4: for c being Point of TOP-REAL 2 st c in U holds |.c-q.| < r/2 by Th30;
  consider p being Point of TOP-REAL 2, V being open Subset of X such that
A5: y in V and
  p in V and
A6: for c being Point of TOP-REAL 2 st c in V holds |.c-p.| < r/2 by Th30;
  take U,V;
  thus U is open & V is open & x in U by A3;
  hereby
    assume y in U;
    then |.b-q.| < r/2 by A4;
    then
A7: |.a-q.|+|.b-q.| < (r/2)+r/2 by A3,A4,XREAL_1:8;
    |.a-b.| <= |.a-q.|+|.q-b.| by TOPRNS_1:34;
    hence contradiction by A7,TOPRNS_1:27;
  end;
  thus y in V by A5;
  assume
A8: x in V;
A9: |.a-b.| <= |.a-p.|+|.p-b.| by TOPRNS_1:34;
  |.b-p.| < r/2 by A5,A6;
  then |.a-p.|+|.b-p.| < (r/2)+r/2 by A8,A6,XREAL_1:8;
  hence contradiction by A9,TOPRNS_1:27;
end;

theorem
  Niemytzki-plane is Tychonoff
proof
  set X = Niemytzki-plane;
  consider B being Neighborhood_System of X such that
A1: for x holds B.(|[x,0]|) = {Ball(|[x,r]|,r) \/ {|[x,0]|} where r is
  Real: r > 0} and
A2: for x,y st y > 0 holds B.(|[x,y]|) = {Ball(|[x,y]|,r) /\ y>=0-plane
  where r is Real: r > 0} by Def3;
  reconsider uB = Union B as prebasis of X by YELLOW_9:27;
A3: the carrier of X = y>=0-plane by Def3;
  now
    let x be Point of X;
    let V be Subset of X;
    assume that
A4: x in V and
A5: V in uB;
    V is open by A5,TOPS_2:def 1;
    then consider V9 being Subset of X such that
A6: V9 in B.x and
A7: V9 c= V by A4,YELLOW_8:def 1;
    x in y>=0-plane by A3;
    then reconsider x9 = x as Point of TOP-REAL 2;
A8: x = |[x9`1,x9`2]| by EUCLID:53;
    per cases by A3,A8,Th18;
    suppose
A9:   x9`2 = 0;
      then B.x = {Ball(|[x9`1,r]|,r) \/ {|[x9`1,0]|}
         where r is Real: r > 0} by A1,A8;
      then consider r being Real such that
A10:  V9 = Ball(|[x9`1,r]|,r)\/{|[x9`1,0]|} and
A11:  r > 0 by A6;
      consider f being continuous Function of Niemytzki-plane, I[01] such that
A12:  f.(|[x9`1,0]|) = 0 and
A13:  for a,b being Real holds (|[a,b]| in V9` implies f.(|[a,
b]|) = 1) & (|[a,b]| in V9\{|[x9`1,0]|} implies f.(|[a,b]|) = |.|[x9`1,0]|-|[a,
      b]|.| ^2/(2*r*b)) by A10,A11,Th76;
      take f;
      thus f.x = 0 by A9,A12,EUCLID:53;
      thus f.:V` c= {1}
      proof
        let u be object;
        assume u in f.:V`;
        then consider b being Point of X such that
A14:    b in V` and
A15:    u = f.b by FUNCT_2:65;
        b in y>=0-plane by A3;
        then reconsider c = b as Element of TOP-REAL 2;
A16:    V` c= V9` by A7,SUBSET_1:12;
        b = |[c`1,c`2]| by EUCLID:53;
        then u = 1 by A16,A14,A13,A15;
        hence thesis by TARSKI:def 1;
      end;
    end;
    suppose
A17:  x9`2 > 0;
      then B.x = {Ball(|[x9`1,x9`2]|,r) /\ y>=0-plane
      where r is Real: r > 0} by A2,A8;
      then consider r being Real such that
A18:  V9 = Ball(|[x9`1,x9`2]|,r)/\y>=0-plane and
A19:  r > 0 by A6;
      consider f being continuous Function of Niemytzki-plane, I[01] such that
A20:  f.(|[x9`1,x9`2]|) = 0 and
A21:  for a,b being Real holds (|[a,b]| in V9` implies f.(|[a,
b]|) = 1) & (|[a,b]| in V9 implies f.(|[a,b]|) = |.|[x9`1,x9`2]|-|[a,b]|.|/r)
      by A17,A18,A19,Th81;
      take f;
      thus f.x = 0 by A20,EUCLID:53;
      thus f.:V` c= {1}
      proof
        let u be object;
        assume u in f.:V`;
        then consider b being Point of X such that
A22:    b in V` and
A23:    u = f.b by FUNCT_2:65;
        b in y>=0-plane by A3;
        then reconsider c = b as Element of TOP-REAL 2;
A24:    V` c= V9` by A7,SUBSET_1:12;
        b = |[c`1,c`2]| by EUCLID:53;
        then u = 1 by A24,A22,A21,A23;
        hence thesis by TARSKI:def 1;
      end;
    end;
  end;
  hence thesis by Th52,Th82;
end;

{"subset_name": "curated", "file": "formal/mizar/topgen_5.miz"}