topgen_5.miz

    begin

    reserve x,y for Real,

u,v,w for set,

r for positive Real;

    theorem :: TOPGEN_5:1



     Th1: for f,g be Function st f tolerates g holds for A be 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, FUNCT_4: 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 :: TOPGEN_5:2

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

    theorem :: TOPGEN_5:3



     Th3: for x,a be set, f be 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 :: TOPGEN_5:4

    for b be set, f be Function holds b in ( dom ( commute f)) iff ex a be set, g be 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 be object such that

         A2: [a, b] in ( dom ( uncurry f)) by A1, XTUPLE_0:def 13;

        consider a9 be object, g be Function, b9 be 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 be set, g be 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 :: TOPGEN_5:5



     Th5: for a,b be set, f be Function holds a in ( dom (( commute f) . b)) iff ex g be 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 be object, g be Function, b be 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 be object, g be Function, b9 be 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 be 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 :: TOPGEN_5:6



     Th6: for a,b be set, f,g be 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 :: TOPGEN_5:7



     Th7: for a be set, f,g,h be 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 be 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 be 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 be 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 :: TOPGEN_5:8



     Th8: for X,Y be 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 be Function such that

       A1: ( dom f) = ( product <*X, Y*>) & for g be 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, FINSEQ_1: 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 be Function such that

           A8: x2 = g2 and

           A9: ( dom g2) = ( dom <*X, Y*>) and for y be object st y in ( dom <*X, Y*>) holds (g2 . y) in ( <*X, Y*> . y) by A1, A6, CARD_3:def 5;

          consider g1 be Function such that

           A10: x1 = g1 and

           A11: ( dom g1) = ( dom <*X, Y*>) and for y be 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 be 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 be object such that

           A13: t in ( dom f) and

           A14: z = (f . t) by FUNCT_1:def 3;

          consider g be Function such that

           A15: t = g and ( dom g) = ( dom <*X, Y*>) and

           A16: for y be 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 :: TOPGEN_5:sch1

    SCH1 { P[ object], A,B,C() -> non empty set , F1,F2( object) -> set } :

ex f be Function of C(), B() st for a be 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 be Element of A() st a in C() holds (P[a] implies F1(a) in B()) & ( not P[a] implies F2(a) in B());



       A3: for a be 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 be Function of C(), B() such that

       A4: for x be 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 :: TOPGEN_5:sch2

    SCH2 { P,Q[ object], A,B,C() -> non empty set , F1,F2,F3( object) -> object } :

ex f be Function of C(), B() st for a be 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 be 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());

      set D = { a where a be Element of C() : P[a] or Q[a] };

      per cases ;

        suppose

         A3: D = {} ;

        consider f be Function such that

         A4: ( dom f) = C() & for u be 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 be 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 be 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 be Element of C() st a = b & (P[b] or Q[b]);

          then a in C();

          hence thesis by A12, A1, A2;

        end;

        consider g be Function of D, B() such that

         A13: for x be 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 be 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 be Function of C(), B() such that

         A18: for x be 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 :: TOPGEN_5:9



     Th9: for a,b be 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 :: TOPGEN_5:10



     Th10: for X be TopSpace, Y be non empty TopSpace holds for A,B be closed Subset of X holds for f be continuous Function of (X | A), Y holds for g be 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 be 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 be 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, XBOOLE_1: 28;

        hence thesis by A12, A9, A11, A6, A13, A14, PRE_TOPC: 13;

      end;

      hence thesis;

    end;

    theorem :: TOPGEN_5:11



     Th11: for X be TopSpace, Y be non empty TopSpace holds for A,B be closed Subset of X st A misses B holds for f be continuous Function of (X | A), Y holds for g be 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 :: TOPGEN_5:12



     Th12: for X be TopSpace, Y be non empty TopSpace holds for A be open closed Subset of X holds for f be continuous Function of (X | A), Y holds for g be 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

    theorem :: TOPGEN_5:13



     Th13: for n be Element of NAT holds for a be Point of ( TOP-REAL n) holds for r be 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

      :: TOPGEN_5:def1

      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;

      :: TOPGEN_5:def2

      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 :: TOPGEN_5:14

    for a,b be 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 :: TOPGEN_5:15



     Th15: for a,b be 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 :: TOPGEN_5:16



     Th16: ( card y=0-line ) = continuum

    proof

      deffunc F( Real) = |[$1, 0 ]|;

      consider f be Function such that

       A1: ( dom f) = REAL and

       A2: for r be 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 be 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 :: TOPGEN_5:17

    for a,b be 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 :: TOPGEN_5:18



     Th18: for a,b be 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 :: TOPGEN_5:19



     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 :: TOPGEN_5:20



     Th20: for a,b,r be 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 :: TOPGEN_5:21



     Th21: for a,b,r be 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 be 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 :: TOPGEN_5:22



     Th22: for n be Element of NAT , a,b be Element of ( TOP-REAL n), r1,r2 be 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 :: TOPGEN_5:23



     Th23: for a be Real, r1,r2 be 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 :: TOPGEN_5:24



     Th24: for T1,T2 be non empty TopSpace holds for B1 be Neighborhood_System of T1 holds for B2 be 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

      ::$Notion-Name

      :: TOPGEN_5:def3

      func Niemytzki-plane -> strict non empty TopSpace means

      : Def3: the carrier of it = y>=0-plane & ex B be Neighborhood_System of it st (for x holds (B . |[x, 0 ]|) = { (( Ball ( |[x, r]|,r)) \/ { |[x, 0 ]|}) where r be Real : r > 0 }) & for x, y st y > 0 holds (B . |[x, y]|) = { (( Ball ( |[x, y]|,r)) /\ y>=0-plane ) where r be 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 be Real : r > 0 };

        set X = y>=0-plane ;

        deffunc F2( Element of ( TOP-REAL 2)) = { (( Ball ($1,r)) /\ X) where r be Real : r > 0 };

        consider B be ManySortedSet of X such that

         A1: for a be 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 be 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 be 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 be 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 be set st x in U & U in (B . y) & y in X holds ex V be 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 be 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 be 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 be set st x in X & U1 in (B . x) & U2 in (B . x) holds ex U be 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 be Real such that

             A31: U1 = (( Ball ( |[(z `1 ), r1]|,r1)) \/ {z}) and

             A32: r1 > 0 by A28;

            consider r2 be 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 be 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 be Real such that

             A38: U1 = (( Ball (z,r1)) /\ X) and r1 > 0 by A28;

            consider r2 be Real such that

             A39: U2 = (( Ball (z,r2)) /\ X) and r2 > 0 by A29, A37;

            r1 <= r2 or r1 >= r2;

            then

            consider U be 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 be 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 be 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 be 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 be Subset-Family of X such that P = ( Union B) and

         A47: for T be TopStruct st the carrier of T = X & the topology of T = ( UniCl P) holds T is TopSpace & for T9 be 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 be Real holds a1(r) = a2(r) by EUCLID: 52;



           A50: { a2(r) where r be Real : R[r] } c= { a1(r1) where r1 be Real : R[r1] }

          proof

            let e be object;

            assume e in { a2(r) where r be Real : R[r] };

            then

            consider r be Real such that

             A51: e = a2(r) & R[r];

            e = a1(r) & R[r] by A49, A51;

            hence e in { a1(r1) where r1 be Real : R[r1] };

          end;

          { a1(r) where r be Real : R[r] } c= { a2(r1) where r1 be Real : R[r1] }

          proof

            let e be object;

            assume e in { a1(r) where r be Real : R[r] };

            then

            consider r be Real such that

             A52: e = a1(r) & R[r];

            e = a2(r) & R[r] by A49, A52;

            hence e in { a2(r1) where r1 be Real : R[r1] };

          end;

          then

           A53: { a1(r) where r be Real : R[r] } = { a2(r) where r be Real : R[r] } by A50;

           P[ |[x, 0 ]|];

          then (B . |[x, 0 ]|) = F1(|[) by A48, A1;

          hence (B . |[x, 0 ]|) = { (( Ball ( |[x, r]|,r)) \/ { |[x, 0 ]|}) where r be 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 be Neighborhood_System of T1 st (for x holds (B . |[x, 0 ]|) = { (( Ball ( |[x, r]|,r)) \/ { |[x, 0 ]|}) where r be Real : r > 0 }) & for x, y st y > 0 holds (B . |[x, y]|) = { (( Ball ( |[x, y]|,r)) /\ y>=0-plane ) where r be Real : r > 0 } and

         A58: the carrier of T2 = y>=0-plane and

         A59: ex B be Neighborhood_System of T2 st (for x holds (B . |[x, 0 ]|) = { (( Ball ( |[x, r]|,r)) \/ { |[x, 0 ]|}) where r be Real : r > 0 }) & for x, y st y > 0 holds (B . |[x, y]|) = { (( Ball ( |[x, y]|,r)) /\ y>=0-plane ) where r be Real : r > 0 };

        consider B2 be Neighborhood_System of T2 such that

         A60: for x holds (B2 . |[x, 0 ]|) = { (( Ball ( |[x, r]|,r)) \/ { |[x, 0 ]|}) where r be Real : r > 0 } and

         A61: for x, y st y > 0 holds (B2 . |[x, y]|) = { (( Ball ( |[x, y]|,r)) /\ y>=0-plane ) where r be Real : r > 0 } by A59;

        consider B1 be Neighborhood_System of T1 such that

         A62: for x holds (B1 . |[x, 0 ]|) = { (( Ball ( |[x, r]|,r)) \/ { |[x, 0 ]|}) where r be Real : r > 0 } and

         A63: for x, y st y > 0 holds (B1 . |[x, y]|) = { (( Ball ( |[x, y]|,r)) /\ y>=0-plane ) where r be 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 be Real : r > 0 } & (B2 . z) = { (( Ball ( |[(z `1 ), r]|,r)) \/ { |[(z `1 ), 0 ]|}) where r be Real : r > 0 } or (z `2 ) > 0 & (B1 . z) = { (( Ball ( |[(z `1 ), (z `2 )]|,r)) /\ y>=0-plane ) where r be Real : r > 0 } & (B2 . z) = { (( Ball ( |[(z `1 ), (z `2 )]|,r)) /\ y>=0-plane ) where r be 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 :: TOPGEN_5:25



     Th25: ( y>=0-plane \ y=0-line ) is open Subset of Niemytzki-plane

    proof

      consider BB be Neighborhood_System of Niemytzki-plane such that for x holds (BB . |[x, 0 ]|) = { (( Ball ( |[x, r]|,r)) \/ { |[x, 0 ]|}) where r be Real : r > 0 } and

       A1: for x, y st y > 0 holds (BB . |[x, y]|) = { (( Ball ( |[x, y]|,r)) /\ y>=0-plane ) where r be 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 be 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 :: TOPGEN_5:26



     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 :: TOPGEN_5:27



     Th27: for x be Real, r be 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 be Neighborhood_System of Niemytzki-plane such that

       A1: for x holds (BB . |[x, 0 ]|) = { (( Ball ( |[x, q]|,q)) \/ { |[x, 0 ]|}) where q be Real : q > 0 } and for x, y st y > 0 holds (BB . |[x, y]|) = { (( Ball ( |[x, y]|,q)) /\ y>=0-plane ) where q be Real : q > 0 } by Def3;

      (BB . |[x, 0 ]|) = { (( Ball ( |[x, q]|,q)) \/ { |[x, 0 ]|}) where q be Real : q > 0 } by A1;

      then (( Ball ( |[x, r]|,r)) \/ { |[x, 0 ]|}) in (BB . a);

      hence thesis by YELLOW_8: 12;

    end;

    theorem :: TOPGEN_5:28



     Th28: for x be Real holds for y,r be 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 be Neighborhood_System of Niemytzki-plane such that for x holds (BB . |[x, 0 ]|) = { (( Ball ( |[x, q]|,q)) \/ { |[x, 0 ]|}) where q be Real : q > 0 } and

       A1: for x, y st y > 0 holds (BB . |[x, y]|) = { (( Ball ( |[x, y]|,q)) /\ y>=0-plane ) where q be Real : q > 0 } by Def3;

      (BB . |[x, y]|) = { (( Ball ( |[x, y]|,q)) /\ y>=0-plane ) where q be Real : q > 0 } by A1;

      then (( Ball ( |[x, y]|,r)) /\ y>=0-plane ) in (BB . a);

      hence thesis by YELLOW_8: 12;

    end;

    theorem :: TOPGEN_5:29



     Th29: for x,y be Real holds for r be 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 :: TOPGEN_5:30



     Th30: for p be Point of Niemytzki-plane holds for r be positive Real holds ex a be Point of ( TOP-REAL 2), U be open Subset of Niemytzki-plane st p in U & a in U & for b be 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 be Neighborhood_System of Niemytzki-plane such that

       A1: for x holds (BB . |[x, 0 ]|) = { (( Ball ( |[x, q]|,q)) \/ { |[x, 0 ]|}) where q be Real : q > 0 } and

       A2: for x, y st y > 0 holds (BB . |[x, y]|) = { (( Ball ( |[x, y]|,q)) /\ y>=0-plane ) where q be 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 be 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 be 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 :: TOPGEN_5:31



     Th31: for x,y be Real holds for r be positive Real holds ex w,v be 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 be 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 be 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 :: TOPGEN_5:32



     Th32: for A be Subset of Niemytzki-plane st A = (( y>=0-plane \ y=0-line ) /\ ( product <* RAT , RAT *>)) holds for x be 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 be Neighborhood_System of Niemytzki-plane such that

       A2: for x holds (BB . |[x, 0 ]|) = { (( Ball ( |[x, q]|,q)) \/ { |[x, 0 ]|}) where q be Real : q > 0 } and

       A3: for x, y st y > 0 holds (BB . |[x, y]|) = { (( Ball ( |[x, y]|,q)) /\ y>=0-plane ) where q be Real : q > 0 } by Def3;



       A4: a = |[(b `1 ), (b `2 )]| by EUCLID: 53;

      for U be 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 be Real : q > 0 } by A2, A4;

          then

          consider q be 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 be 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 be 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 be Real : q > 0 } by A3, A4;

          then

          consider q be 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 be 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 be 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 :: TOPGEN_5:33



     Th33: for A be Subset of Niemytzki-plane st A = ( y>=0-plane \ y=0-line ) holds for x be 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, XBOOLE_1: 33;

      then ( Cl (B \ {s})) c= ( Cl (A \ {s})) by PRE_TOPC: 19;

      hence thesis by A1, Th32;

    end;

    theorem :: TOPGEN_5:34



     Th34: for A be 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 :: TOPGEN_5:35



     Th35: for A be 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 :: TOPGEN_5:36



     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 :: TOPGEN_5:37

    (( 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 :: TOPGEN_5:38

    ( 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 :: TOPGEN_5:39

    ( 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 :: TOPGEN_5:40

     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 :: TOPGEN_5:41



     Th41: for A be Subset of Niemytzki-plane st A = y=0-line holds ( Der A) is empty

    proof

      consider BB be Neighborhood_System of Niemytzki-plane such that

       A1: for x holds (BB . |[x, 0 ]|) = { (( Ball ( |[x, r]|,r)) \/ { |[x, 0 ]|}) where r be Real : r > 0 } and for x, y st y > 0 holds (BB . |[x, y]|) = { (( Ball ( |[x, y]|,r)) /\ y>=0-plane ) where r be Real : r > 0 } by Def3;

      let A be Subset of Niemytzki-plane ;

      assume that

       A2: A = y=0-line and

       A3: not ( Der A) is 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 be 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 be 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 :: TOPGEN_5:42



     Th42: for A be 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 :: TOPGEN_5:43



     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 be Subset-Family of REAL such that

       A1: the topology of Sorgenfrey-line = ( UniCl B) and

       A2: B = { [.x, q.[ where x,q be 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 be Real such that

           A4: C = [.y, q.[ and

           A5: y < q and q is rational by A2;

          assume x in C;

          consider r be 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 :: TOPGEN_5:44

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

    theorem :: TOPGEN_5:45

     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 :: TOPGEN_5:46

     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 be Point of ( TOP-REAL 2), Up be open Subset of T such that

       A4: p in Up and ap in Up and

       A5: for b be Point of ( TOP-REAL 2) st b in Up holds |.(b - ap).| < (r / 2) by Th30;

      consider aq be Point of ( TOP-REAL 2), Uq be open Subset of T such that

       A6: q in Uq and aq in Uq and

       A7: for b be 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 :: TOPGEN_5:47

     not Niemytzki-plane is 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 be set, U,V be 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 be Subset of T st W <> {} & V <> {} & W is closed & V is closed & W misses V holds ex P,Q be Subset of T st P is open & Q is open & W c= P & V c= Q & P misses Q;



       A4: for a be object st a in ( bool y=0-line ) holds ex b be 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 be 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 be Function such that

       A14: ( dom G) = ( bool y=0-line ) and

       A15: for a be 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 be 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 be set, UB,VB be 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 be set, UA,VA be 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 be object st z in C & z in (UA /\ VB)) or ex z be object st z in C & z in (UB /\ VA) by XBOOLE_0: 3;

        then

        consider z be 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 be 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

    definition

      let T be TopSpace;

      :: TOPGEN_5:def4

      attr T is Tychonoff means for A be closed Subset of T, a be Point of T st a in (A ` ) holds ex f be 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 be closed Subset of T, a be Point of T st a in (A ` ) holds ex f be 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, XXREAL_1: 36;

        reconsider A, B as open Subset of I[01] by TOPALG_1: 4, TOPALG_1: 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 be 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 be 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 be continuous Function of T, ( Closed-Interval-TSpace (( - 1),1)) such that

           A19: (g | B) = h by A11, TIETZE: 23;

          consider p be Function of I[01] , ( Closed-Interval-TSpace (( - 1),1)) such that

           A20: p is being_homeomorphism and for r be 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 :: TOPGEN_5:48

    for X be T_1 TopSpace st X is Tychonoff holds for B be prebasis of X holds for x be Point of X holds for V be Subset of X st x in V & V in B holds ex f be 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 :: TOPGEN_5:49



     Th49: for X be TopSpace, R be non empty SubSpace of R^1 holds for f,g be continuous Function of X, R holds for A be Subset of X st for x be 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 be 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 :: TOPGEN_5:50



     Th50: for X be TopSpace, R be non empty SubSpace of R^1 holds for f,g be continuous Function of X, R holds ex h be continuous Function of X, R st for x be 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 be Subset of X such that

       A1: for a be 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 be Subset of X such that

       A2: for a be 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: not X is empty & not A is empty & not B is empty;

        then

        reconsider X9 = X as non empty TopSpace;

        for x be 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, FUNCT_4: 15;

        hence thesis by XXREAL_0:def 10;

      end;

    end;

    theorem :: TOPGEN_5:51



     Th51: for X be non empty TopSpace, R be non empty SubSpace of R^1 holds for A be finite non empty set holds for F be ManySortedFunction of A st for a be set st a in A holds (F . a) is continuous Function of X, R holds ex f be continuous Function of X, R st for x be Point of X, S be 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 be continuous Function of X, R st for x be Point of X, S be 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 be 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 be 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 not (B \/ {x}) is 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 be continuous Function of X, R such that

           A13: for x be Point of X, S be finite non empty Subset of REAL st S = ( rng (( commute (F | B9)) . x)) holds (f . x) = ( max S) by A8;

          consider h be continuous Function of X, R such that

           A14: for x be 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 not (B \/ {x}) is 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 :: TOPGEN_5:52



     Th52: for X be T_1 non empty TopSpace holds for B be prebasis of X st for x be Point of X holds for V be Subset of X st x in V & V in B holds ex f be 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 be Point of X holds for V be Subset of X st x in V & V in BB holds ex f be 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 be 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 be 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 be Subset of X, f be 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 be object st x in F holds ex y be 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 be 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 be Function such that

         A14: ( dom G) = F & for x be 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 be 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 be continuous Function of X, I[01] such that

         A18: for x be Point of X, S be 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 be 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 be 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 be Subset of X, g be 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 be 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 :: TOPGEN_5:53



     Th53: Sorgenfrey-line is T_1

    proof

      set T = Sorgenfrey-line ;

      consider B be Subset-Family of REAL such that

       A1: the topology of Sorgenfrey-line = ( UniCl B) and

       A2: B = { [.x, q.[ where x,q be 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 be 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 be 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 be 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 be 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 :: TOPGEN_5:54



     Th54: for x be 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, XXREAL_1: 294;

      hence thesis;

    end;

    theorem :: TOPGEN_5:55

    for x be 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, XXREAL_1: 288;

      hence thesis;

    end;

    theorem :: TOPGEN_5:56



     Th56: for x be 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, XXREAL_1: 294;

      hence thesis;

    end;

    theorem :: TOPGEN_5:57



     Th57: for x,y be 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, XXREAL_1: 294

      .= (A /\ B) by XXREAL_1: 224, XXREAL_1: 294;

      hence thesis;

    end;

    theorem :: TOPGEN_5:58



     Th58: for x be Real, w be Rational holds ex f be continuous Function of Sorgenfrey-line , I[01] st for a be 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;

      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 be 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 be Function of X, I[01] such that

       A2: for a be 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 :: TOPGEN_5:59

     Sorgenfrey-line is Tychonoff

    proof

      set X = Sorgenfrey-line ;



       A1: the carrier of X = REAL by TOPGEN_3:def 2;

      consider B be Subset-Family of REAL such that

       A2: the topology of X = ( UniCl B) and

       A3: B = { [.x, q.[ where x,q be 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 be Real such that

         A6: V = [.a, q.[ and a < q and

         A7: q is rational by A5, A3;

        consider f be continuous Function of X, I[01] such that

         A8: for b be 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 be 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

    definition

      let x be Real, r be positive Real;

      :: TOPGEN_5:def5

      func + (x,r) -> Function of Niemytzki-plane , I[01] means

      : Def5: (it . |[x, 0 ]|) = 0 & for a be Real, b be 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 be 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 be Function of Niemytzki-plane , I[01] such that

         A9: for a be 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 be Real, b be 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 be Real, b be 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 :: TOPGEN_5:60



     Th60: for p be Point of ( TOP-REAL 2) st (p `2 ) >= 0 holds for x be Real, r be 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 :: TOPGEN_5:61



     Th61: for x,y be Real, r be 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 :: TOPGEN_5:62



     Th62: for p be Point of ( TOP-REAL 2) holds for x be Real, a,r be 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 :: TOPGEN_5:63



     Th63: for p be Point of ( TOP-REAL 2) holds for x,a be Real, r be 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 :: TOPGEN_5:64



     Th64: for p be Point of ( TOP-REAL 2) st (p `2 ) >= 0 holds for x,a be Real, r be 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 :: TOPGEN_5:65



     Th65: for p be Point of ( TOP-REAL 2) st (p `2 ) >= 0 holds for x,a,b be Real, r be positive Real st 0 <= a & b <= 1 & (( + (x,r)) . p) in ].a, b.[ holds ex r1 be 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;

      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 :: TOPGEN_5:66



     Th66: for x be Real, a,r be 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 :: TOPGEN_5:67



     Th67: for x be Real, a,r be 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 :: TOPGEN_5:68



     Th68: for p be Point of ( TOP-REAL 2) st (p `2 ) >= 0 holds for x,a be Real, r be 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 :: TOPGEN_5:69



     Th69: for p be Point of ( TOP-REAL 2) st (p `2 ) > 0 holds for x,a be Real, r be positive Real st 0 <= a & a < (( + (x,r)) . p) holds ex r1 be 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 :: TOPGEN_5:70



     Th70: for p be Point of ( TOP-REAL 2) st (p `2 ) = 0 holds for x be Real, r be positive Real st (( + (x,r)) . p) = 1 holds ex r1 be 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 :: TOPGEN_5:71



     Th71: for T be non empty TopSpace, S be SubSpace of T holds for B be Basis of T holds { (A /\ ( [#] S)) where A be 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 be 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 be 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 be 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 be 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 be 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 :: TOPGEN_5:72



     Th72: { ].a, b.[ where a,b be Real : a < b } is Basis of R^1

    proof

      set X = { ].a, b.[ where a,b be Real : a < b };

      X c= ( bool REAL )

      proof

        let u be object;

        assume u in X;

        then ex a,b be 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 be 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 be 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 :: TOPGEN_5:73



     Th73: for T be TopSpace holds for U,V be Subset of T holds for B be 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 be 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 be 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 :: TOPGEN_5:74



     Th74: (({ [. 0 , a.[ where a be Real : 0 < a & a <= 1 } \/ { ].a, 1.] where a be Real : 0 <= a & a < 1 }) \/ { ].a, b.[ where a,b be 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, XXREAL_1: 36;

      reconsider B = { ].a, b.[ where a,b be Real : a < b } as Basis of R^1 by Th72;

      set S = I[01] , T = R^1 ;

      set A1 = { [. 0 , a.[ where a be Real : 0 < a & a <= 1 };

      set A2 = { ].a, 1.] where a be Real : 0 <= a & a < 1 };

      set A3 = { ].a, b.[ where a,b be Real : 0 <= a & a < b & b <= 1 };

      set B9 = { (A /\ ( [#] S)) where A be 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 be Subset of T such that

           A2: u = (A /\ ( [#] S)) and

           A3: A in B and

           A4: A meets ( [#] S);

          consider x be object such that

           A5: x in A and

           A6: x in ( [#] S) by A4, XBOOLE_0: 3;

          consider a,b be 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 be 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 be 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 be 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 :: TOPGEN_5:75



     Th75: for T be non empty TopSpace holds for f be Function of T, I[01] holds f is continuous iff for a,b be 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 be Real : 0 <= a & a < b & b <= 1 };

      set A2 = { ].a, 1.] where a be Real : 0 <= a & a < 1 };

      set A1 = { [. 0 , a.[ where a be 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 be 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 be Real st A = [. 0 , a.[ & 0 < a & a <= 1;

          hence (f " A) is open by A7;

        end;

          suppose A in A2;

          then ex a be 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 be 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 be Neighborhood_System of Niemytzki-plane such that

         A1: for x holds (BB . |[x, 0 ]|) = { (( Ball ( |[x, q]|,q)) \/ { |[x, 0 ]|}) where q be Real : q > 0 } and

         A2: for x, y st y > 0 holds (BB . |[x, y]|) = { (( Ball ( |[x, y]|,q)) /\ y>=0-plane ) where q be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 :: TOPGEN_5:76



     Th76: for U be Subset of Niemytzki-plane holds for x, r st U = (( Ball ( |[x, r]|,r)) \/ { |[x, 0 ]|}) holds ex f be continuous Function of Niemytzki-plane , I[01] st (f . |[x, 0 ]|) = 0 & for a,b be 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;

    definition

      let x,y be Real, r be positive Real;

      :: TOPGEN_5:def6

      func + (x,y,r) -> Function of Niemytzki-plane , I[01] means

      : Def6: for a be Real, b be 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 be 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 be Function of Niemytzki-plane , I[01] such that

         A4: for a be 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 be Real, b be 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 be Real, b be 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 :: TOPGEN_5:77



     Th77: for p be Point of ( TOP-REAL 2) st (p `2 ) >= 0 holds for x be Real, y be non negative Real holds for r be 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 :: TOPGEN_5:78



     Th78: for x be Real, y be non negative Real holds for r,a be 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 :: TOPGEN_5:79



     Th79: for p be Point of ( TOP-REAL 2) st (p `2 ) > 0 holds for x be Real, a be non negative Real holds for y,r be 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 :: TOPGEN_5:80



     Th80: for p be Point of ( TOP-REAL 2) st (p `2 ) = 0 holds for x be Real, a be non negative Real holds for y,r be positive Real st (( + (x,y,r)) . p) > a holds |.( |[x, y]| - p).| > (r * a) & ex r1 be 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 be Neighborhood_System of Niemytzki-plane such that

         A1: for x holds (BB . |[x, 0 ]|) = { (( Ball ( |[x, q]|,q)) \/ { |[x, 0 ]|}) where q be Real : q > 0 } and

         A2: for x, y st y > 0 holds (BB . |[x, y]|) = { (( Ball ( |[x, y]|,q)) /\ y>=0-plane ) where q be 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 be 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 be 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 be 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 :: TOPGEN_5:81



     Th81: for U be Subset of Niemytzki-plane holds for x, y, r st y > 0 & U = (( Ball ( |[x, y]|,r)) /\ y>=0-plane ) holds ex f be continuous Function of Niemytzki-plane , I[01] st (f . |[x, y]|) = 0 & for a,b be 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 :: TOPGEN_5:82



     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 be Point of ( TOP-REAL 2), U be open Subset of X such that

       A3: x in U and q in U and

       A4: for c be Point of ( TOP-REAL 2) st c in U holds |.(c - q).| < (r / 2) by Th30;

      consider p be Point of ( TOP-REAL 2), V be open Subset of X such that

       A5: y in V and p in V and

       A6: for c be 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 :: TOPGEN_5:83

     Niemytzki-plane is Tychonoff

    proof

      set X = Niemytzki-plane ;

      consider B be Neighborhood_System of X such that

       A1: for x holds (B . |[x, 0 ]|) = { (( Ball ( |[x, r]|,r)) \/ { |[x, 0 ]|}) where r be Real : r > 0 } and

       A2: for x, y st y > 0 holds (B . |[x, y]|) = { (( Ball ( |[x, y]|,r)) /\ y>=0-plane ) where r be 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 be 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 be Real : r > 0 } by A1, A8;

          then

          consider r be Real such that

           A10: V9 = (( Ball ( |[(x9 `1 ), r]|,r)) \/ { |[(x9 `1 ), 0 ]|}) and

           A11: r > 0 by A6;

          consider f be continuous Function of Niemytzki-plane , I[01] such that

           A12: (f . |[(x9 `1 ), 0 ]|) = 0 and

           A13: for a,b be 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 be 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 be Real : r > 0 } by A2, A8;

          then

          consider r be Real such that

           A18: V9 = (( Ball ( |[(x9 `1 ), (x9 `2 )]|,r)) /\ y>=0-plane ) and

           A19: r > 0 by A6;

          consider f be continuous Function of Niemytzki-plane , I[01] such that

           A20: (f . |[(x9 `1 ), (x9 `2 )]|) = 0 and

           A21: for a,b be 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 be 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;