topgen_6.miz



    begin

    

     Lm1: for f be Function, x,y be set st x in (f " {y}) holds (f . x) = y

    proof

      let f be Function, x,y be set such that

       A1: x in (f " {y});

      (f . x) in {y} by A1, FUNCT_1:def 7;

      hence (f . x) = y by TARSKI:def 1;

    end;

    reserve T for TopSpace,

x,y,a,b,U,Ux,rx for set,

p,q for Rational,

F,G for Subset-Family of T,

Us,I for Subset-Family of Sorgenfrey-line ;

    

     Lm2: Sorgenfrey-line is T_2

    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;

        consider q be Rational such that

         A6: b < q and q < (b + 1) by RAT_1: 7, XREAL_1: 29;

         [.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;

        

         A10: (U /\ V) = {}

        proof

          thus (U /\ V) c= {}

          proof

            let p be object;

            assume

             A11: p in (U /\ V);

            then

            reconsider d = p as ExtReal;

            d in [.a, w.[ & d in [.b, q.[ by XBOOLE_0:def 4, A11;

            then d < w & b <= d by XXREAL_1: 3;

            hence p in {} by A9, XXREAL_0: 2;

          end;

          thus {} c= (U /\ V) by XBOOLE_1: 2;

        end;

        thus U is open & V is open;

        thus thesis by A6, A8, XXREAL_1: 3, A10, XBOOLE_0:def 7;

      end;

        suppose

         A12: a > b;

        consider q be Rational such that

         A13: a < q and q < (a + 1) by RAT_1: 7, XREAL_1: 29;

         [.a, q.[ in B by A2, A13;

        then

         A14: [.a, q.[ in the topology of T by A3;

        consider w be Rational such that

         A15: b < w and

         A16: w < a by A12, RAT_1: 7;

         [.b, w.[ in B by A2, A15;

        then [.b, w.[ in the topology of T by A3;

        then

        reconsider V = [.b, w.[, U = [.a, q.[ as open Subset of T by A14, PRE_TOPC:def 2;

        take U, V;

        

         A17: (U /\ V) = {}

        proof

          thus (U /\ V) c= {}

          proof

            let p be object;

            assume

             A18: p in (U /\ V);

            then

            reconsider d = p as ExtReal;

            d in [.a, q.[ & d in [.b, w.[ by XBOOLE_0:def 4, A18;

            then d < w & a <= d by XXREAL_1: 3;

            hence p in {} by A16, XXREAL_0: 2;

          end;

          thus {} c= (U /\ V)

          proof

            let p be object;

            assume p in {} ;

            hence thesis;

          end;

        end;

        thus U is open & V is open;

        thus thesis by A15, A13, XXREAL_1: 3, A17, XBOOLE_0:def 7;

      end;

    end;

    registration

      cluster Sorgenfrey-line -> T_2;

      coherence by Lm2;

    end

    theorem :: TOPGEN_6:1

    

     Th1: for x,a,b be Real st x in ].a, b.[ holds ex p,r be Rational st x in ].p, r.[ & ].p, r.[ c= ].a, b.[

    proof

      let x,a,b be Real such that

       A1: x in ].a, b.[;

      

       A2: x > a & x < b by XXREAL_1: 4, A1;

      consider p be Rational such that

       A3: p > a & x > p by A2, RAT_1: 7;

      consider r be Rational such that

       A4: x < r & r < b by A2, RAT_1: 7;

      take p, r;

      thus x in ].p, r.[ by A3, A4, XXREAL_1: 4;

      thus ].p, r.[ c= ].a, b.[

      proof

        let y be object;

        assume

         A5: y in ].p, r.[;

        then

        reconsider y1 = y as Element of REAL ;

        y1 > p & y1 < r by XXREAL_1: 4, A5;

        then y1 > a & y1 < b by A3, A4, XXREAL_0: 2;

        hence y in ].a, b.[ by XXREAL_1: 4;

      end;

    end;

    

     Lm3: for T be SubSpace of R^1 holds T is Lindelof

    proof

      let T be SubSpace of R^1 ;

      let U be Subset-Family of T such that

       A1: U is open and

       A2: U is Cover of T;

      per cases ;

        suppose

         A3: the carrier of T = {} ;

        reconsider G = {} as Subset-Family of T by XBOOLE_1: 2;

        take G;

        thus G c= U by XBOOLE_1: 2;

        thus G is Cover of T

        proof

          let x be object;

          assume x in the carrier of T;

          hence thesis by A3;

        end;

        thus G is countable;

      end;

        suppose

         A4: the carrier of T <> {} ;

        

         A5: ( card [: RAT , RAT :]) c= omega by CARD_3:def 14, CARD_4: 7;

        set Q = the set of all ].p, r.[ where p,r be Rational;

        defpred P[ object, object] means ex a,b be Rational st $1 = ].a, b.[ & $2 = [a, b];

        

         A6: for x be object st x in Q holds ex y be object st y in [: RAT , RAT :] & P[x, y]

        proof

          let x be object;

          assume x in Q;

          then

          consider a,b be Rational such that

           A7: x = ].a, b.[;

          take y = [a, b];

          a in RAT & b in RAT by RAT_1:def 2;

          hence y in [: RAT , RAT :] by ZFMISC_1:def 2;

          thus P[x, y] by A7;

        end;

        consider h be Function of Q, [: RAT , RAT :] such that

         A8: for x be object st x in Q holds P[x, (h . x)] from FUNCT_2:sch 1( A6);

        

         A9: ( rng h) c= [: RAT , RAT :];

        

         A10: ( dom h) = Q by FUNCT_2:def 1;

        h is one-to-one

        proof

          let x1,x2 be object such that

           A11: x1 in ( dom h) and

           A12: x2 in ( dom h) and

           A13: (h . x1) = (h . x2);

          consider p1,r1 be Rational such that

           A14: x1 = ].p1, r1.[ and

           A15: (h . x1) = [p1, r1] by A8, A11;

          consider p2,r2 be Rational such that

           A16: x2 = ].p2, r2.[ and

           A17: (h . x2) = [p2, r2] by A8, A12;

          p1 = p2 & r1 = r2 by XTUPLE_0: 1, A13, A15, A17;

          hence x1 = x2 by A14, A16;

        end;

        then ( card Q) c= ( card [: RAT , RAT :]) by CARD_1: 10, A9, A10;

        then

         A18: Q is countable by CARD_3:def 14, A5, XBOOLE_1: 1;

        defpred Pf[ object, object] means ex S be set st S = $2 & $1 in S & $2 in U;

        

         A19: for x be object st x in the carrier of T holds ex y be object st y in U & Pf[x, y]

        proof

          let x be object such that

           A20: x in the carrier of T;

          x in ( union U) by SETFAM_1:def 11, A2, A20, TARSKI:def 3;

          then

          consider Ux be set such that

           A21: x in Ux & Ux in U by TARSKI:def 4;

          thus thesis by A21;

        end;

        consider f be Function of the carrier of T, U such that

         A22: for x be object st x in the carrier of T holds Pf[x, (f . x)] from FUNCT_2:sch 1( A19);

        

         A23: U <> {}

        proof

          assume

           A24: U = {} ;

          the carrier of T c= ( union U) by A2, SETFAM_1:def 11;

          hence contradiction by A24, ZFMISC_1: 2, A4;

        end;

        defpred Pf1[ object, object] means ex S be set st S = $2 & $2 in Q & $1 in S & (S /\ ( [#] T)) c= (f . $1);

        

         A25: for x be object st x in the carrier of T holds ex y be object st y in Q & Pf1[x, y]

        proof

          let x be object such that

           A26: x in the carrier of T;

          

           A27: Pf[x, (f . x)] by A22, A26;

          reconsider Ux = (f . x) as Subset of T by A27;

          Ux is open by A27, A1, TOPS_2:def 1;

          then

          consider Vx be Subset of R^1 such that

           A28: Vx in the topology of R^1 & Ux = (Vx /\ ( [#] T)) by PRE_TOPC:def 4;

          reconsider x as Real by A26;

          Ux c= Vx by A28, XBOOLE_1: 17;

          then

          consider r1 be Real such that

           A29: r1 > 0 & ].(x - r1), (x + r1).[ c= Vx by A27, FRECHET: 8, A28, PRE_TOPC:def 2;

          set a = (x - r1), b = (x + r1);

          

           A30: x < (x + r1) by XREAL_1: 29, A29;

          x > (x - r1) by XREAL_1: 44, A29;

          then

          consider p1,p2 be Rational such that

           A31: x in ].p1, p2.[ & ].p1, p2.[ c= ].a, b.[ by Th1, A30, XXREAL_1: 4;

          set q = ].p1, p2.[;

          

           A32: q c= Vx by A29, A31, XBOOLE_1: 1;

          take q;

          thus q in Q;

          take q;

          thus thesis by A28, A31, A32, XBOOLE_1: 26;

        end;

        consider f1 be Function of the carrier of T, Q such that

         A33: for x be object st x in the carrier of T holds Pf1[x, (f1 . x)] from FUNCT_2:sch 1( A25);

        deffunc F( object) = (f . the Element of (f1 " {$1}));

         ].2, 1.[ in Q;

        then

         A34: ( dom f1) = the carrier of T by FUNCT_2:def 1;

        

         A35: for x be object st x in ( rng f1) holds F(x) in U

        proof

          let x be object such that

           A36: x in ( rng f1);

          (f1 " {x}) <> {} by A36, FUNCT_1: 72;

          then

           A37: the Element of (f1 " {x}) in (f1 " {x});

           the Element of (f1 " {x}) in the carrier of T by A37;

          then the Element of (f1 " {x}) in ( dom f) by A23, FUNCT_2:def 1;

          then F(x) in ( rng f) by FUNCT_1: 3;

          hence thesis;

        end;

        consider g be Function of ( rng f1), U such that

         A38: for q be object st q in ( rng f1) holds (g . q) = F(q) from FUNCT_2:sch 2( A35);

        

         A39: ( card ( rng f1)) c= omega by CARD_3:def 14, A18;

        

         A40: ( dom g) = ( rng f1) by FUNCT_2:def 1, A23;

        then

         A41: ( card ( rng g)) c= ( card ( rng f1)) by CARD_1: 12;

        reconsider G = ( rng g) as Subset-Family of T by TOPS_2: 2;

        take G;

        thus G c= U;

        thus G is Cover of T

        proof

          let x be object;

          assume

           A42: x in the carrier of T;

          set q = (f1 . x);

          

           A43: [x, q] in f1 by FUNCT_1:def 2, A42, A34;

          

           A44: q in {q} by TARSKI:def 1;

          

           A45: q in ( rng f1) by FUNCT_1: 3, A34, A42;

          

           A46: Pf1[x, (f1 . x)] by A33, A42;

          set y = the Element of (f1 " {q});

          

           A47: (f1 " {q}) <> {} by A45, A43, A44, RELAT_1: 131;

          then

           A48: x in (f1 . y) by A46, Lm1;

          

           A49: (f . y) = (g . q) by A38, FUNCT_1: 3, A34, A42;

          y in (f1 " {q}) by A47;

          then

           A50: Pf1[y, (f1 . y)] by A33;

          

           A51: x in ((f1 . y) /\ ( [#] T)) by A42, A48, XBOOLE_0:def 4;

          (g . q) in ( rng g) by FUNCT_1: 3, A45, A40;

          hence x in ( union G) by A51, TARSKI:def 4, A49, A50;

        end;

        thus G is countable by A41, CARD_3:def 14, A39, XBOOLE_1: 1;

      end;

    end;

    registration

      cluster -> Lindelof for SubSpace of R^1 ;

      coherence by Lm3;

    end

    

     Lm4: for p,r be Real st r > p holds ex q be Rational st q in [.p, r.[

    proof

      let p,r be Real such that

       A1: r > p;

      consider q be Rational such that

       A2: p < q & q < r by A1, RAT_1: 7;

      thus thesis by A2, XXREAL_1: 3;

    end;

    

     Lm5: the carrier of Sorgenfrey-line = REAL by TOPGEN_3:def 2;

    consider BB be Subset-Family of REAL such that

     Lm6: the topology of Sorgenfrey-line = ( UniCl BB) and

     Lm7: BB = { [.x, q.[ where x,q be Real : x < q & q is rational } by TOPGEN_3:def 2;

    

     Lm8: BB is Basis of Sorgenfrey-line by Lm5, Lm6, CANTOR_1: 1, CANTOR_1:def 2, TOPS_2: 64;

    

     Lm9: Sorgenfrey-line is Lindelof

    proof

      set S = Sorgenfrey-line ;

      let U be Subset-Family of S such that

       A1: U is open and

       A2: U is Cover of S;

      

       A3: U <> {}

      proof

        assume

         A4: U = {} ;

        the carrier of S c= ( union U) by SETFAM_1:def 11, A2;

        hence contradiction by A4, ZFMISC_1: 2;

      end;

      set V = { ( Int u) where u be Subset of R^1 : u in U };

      set W = ( union V);

      reconsider K = (( [#] S) \ W) as set;

      V is non empty Subset-Family of R^1

      proof

        consider u be object such that

         A5: u in U by XBOOLE_0:def 1, A3;

        reconsider u as Subset of R^1 by TOPGEN_3:def 2, TOPMETR: 17, A5;

        set v = ( Int u);

        

         A6: V c= ( bool ( [#] R^1 ))

        proof

          let x be object such that

           A7: x in V;

          consider u be Subset of R^1 such that

           A8: ( Int u) = x and u in U by A7;

          thus x in ( bool ( [#] R^1 )) by A8;

        end;

        v in V by A5;

        hence thesis by A6;

      end;

      then

      reconsider V as non empty Subset-Family of R^1 ;

      W c= ( [#] R^1 )

      proof

        let x be object;

        assume x in W;

        then

        consider v be set such that

         A9: x in v and

         A10: v in V by TARSKI:def 4;

        thus x in ( [#] R^1 ) by A9, A10;

      end;

      then

      reconsider W as Subset of R^1 ;

      defpred Ph[ object, object] means ex y be Subset of R^1 st $2 = y & y in U & $1 = ( Int y);

      

       A11: for x be object st x in V holds ex y be object st y in U & Ph[x, y]

      proof

        let x be object such that

         A12: x in V;

        consider u be Subset of R^1 such that

         A13: x = ( Int u) and

         A14: u in U by A12;

        take u;

        thus u in U by A14;

        thus Ph[x, u] by A13, A14;

      end;

      consider h be Function of V, U such that

       A15: for x be object st x in V holds Ph[x, (h . x)] from FUNCT_2:sch 1( A11);

      

       A16: for x be Element of V, hx be Subset of R^1 st hx = (h . x) holds x = ( Int hx)

      proof

        let x be Element of V, hx be Subset of R^1 such that

         A17: hx = (h . x);

        consider y be Subset of R^1 such that

         A18: (h . x) = y and y in U and

         A19: x = ( Int y) by A15;

        thus x = ( Int hx) by A18, A19, A17;

      end;

      reconsider T = ( R^1 | W) as SubSpace of R^1 ;

      V c= ( bool ( [#] T))

      proof

        let x be object such that

         A20: x in V;

        reconsider xx = x as set by TARSKI: 1;

        xx c= W

        proof

          let y be object;

          thus thesis by TARSKI:def 4, A20;

        end;

        then xx c= ( [#] T) by PRE_TOPC:def 5;

        hence x in ( bool ( [#] T));

      end;

      then

      reconsider V1 = V as non empty Subset-Family of T;

      

       A21: V1 is open

      proof

        let v be Subset of T such that

         A22: v in V1;

        consider u be Subset of R^1 such that

         A23: v = ( Int u) and u in U by A22;

        

         A24: v in the topology of R^1 by A23, PRE_TOPC:def 2;

        (v /\ ( [#] T)) = v

        proof

          thus (v /\ ( [#] T)) c= v by XBOOLE_1: 17;

          thus v c= (v /\ ( [#] T)) by XBOOLE_1: 19;

        end;

        hence v is open by A24, PRE_TOPC:def 4;

      end;

      

       A25: the carrier of T c= ( union V)

      proof

        let x be object;

        assume x in the carrier of T;

        then x in ( [#] T);

        hence x in ( union V) by PRE_TOPC:def 5;

      end;

      consider B be Subset-Family of T such that

       A26: B c= V and

       A27: B is Cover of T and

       A28: B is countable by METRIZTS:def 2, A21, A25, SETFAM_1:def 11;

      deffunc Ff( object) = (h . $1);

      

       A29: for x be object st x in B holds Ff(x) in U

      proof

        let x be object;

        assume x in B;

        then (h . x) in ( rng h) by A3, FUNCT_2: 4, A26;

        hence (h . x) in U;

      end;

      consider f be Function of B, U such that

       A30: for x be object st x in B holds (f . x) = Ff(x) from FUNCT_2:sch 2( A29);

      reconsider Y = ( rng f) as Subset-Family of S by TOPS_2: 2;

      

       A31: Y is Cover of W

      proof

        let x be object;

        assume

         A32: x in W;

        B is Cover of ( [#] T) by A27;

        then B is Cover of W by PRE_TOPC:def 5;

        then x in ( union B) by A32, SETFAM_1:def 11, TARSKI:def 3;

        then

        consider b be set such that

         A33: x in b & b in B by TARSKI:def 4;

        B = ( dom f) by FUNCT_2:def 1, A3;

        then

         A34: (f . b) in Y by FUNCT_1: 3, A33;

        b c= (f . b)

        proof

          let x be object such that

           A35: x in b;

          

           A36: (f . b) = (h . b) by A30, A33;

          reconsider b1 = b as Element of V qua set by A26, A33;

          (h . b1) in U by A3;

          then

          reconsider hb = (h . b1) as Subset of R^1 by TOPGEN_3:def 2, TOPMETR: 17;

          

           A37: b1 = ( Int hb) by A16;

          b1 c= hb by A37, TOPS_1: 16;

          hence x in (f . b) by A36, A35;

        end;

        hence x in ( union Y) by A34, TARSKI:def 4, A33;

      end;

      

       A38: ( card B) c= omega by CARD_3:def 14, A28;

      ( dom f) = B by FUNCT_2:def 1, A3;

      then ( card ( rng f)) c= ( card B) by CARD_1: 12;

      then

       A39: Y is countable by CARD_3:def 14, A38, XBOOLE_1: 1;

      defpred Pg[ object, object] means ex S be set st S = $2 & $1 in S;

      

       A40: for x be object st x in K holds ex y be object st y in U & Pg[x, y]

      proof

        let x be object;

        assume x in K;

        then x in ( union U) by SETFAM_1:def 11, A2, TARSKI:def 3;

        then

        consider Ux be set such that

         A41: x in Ux and

         A42: Ux in U by TARSKI:def 4;

        take Ux;

        thus Ux in U by A42;

        thus Pg[x, Ux] by A41;

      end;

      consider g be Function of K, U such that

       A43: for x be object st x in K holds Pg[x, (g . x)] from FUNCT_2:sch 1( A40);

      set Q = { [.p, r.[ where p,r be Real : r > p };

      defpred Pk[ object, object] means ex S be set st S = $2 & S c= (g . $1) & ex x,rx be Real st $1 = x & $2 = [.x, rx.[;

      

       A44: for x be object st x in K holds ex y be object st y in Q & Pk[x, y]

      proof

        let x be object such that

         A45: x in K;

        (g . x) in U by FUNCT_2: 5, A45, A3;

        then

        reconsider gx = (g . x) as open Subset of S by A1, TOPS_2:def 1;

        reconsider x1 = x as Point of S by A45;

         Pg[x, (g . x)] by A43, A45;

        then

        consider a be Subset of S such that

         A46: a in BB and

         A47: x1 in a and

         A48: a c= gx by YELLOW_9: 31, Lm8;

        consider p,r be Real such that

         A49: a = [.p, r.[ and r > p and r is rational by Lm7, A46;

        reconsider x2 = x1 as Real by A47, A49;

        

         A50: p <= x2 & x2 < r by A47, A49, XXREAL_1: 3;

        set y = [.x2, r.[;

        take y;

        

         A51: y c= a

        proof

          let z be object such that

           A52: z in y;

          reconsider z1 = z as Real by A52;

          x2 <= z1 & z1 < r by A52, XXREAL_1: 3;

          then p <= z1 & z1 < r by A50, XXREAL_0: 2;

          hence z in a by A49, XXREAL_1: 3;

        end;

        thus y in Q by A50;

        thus Pk[x, y] by A51, A48, XBOOLE_1: 1;

      end;

      consider k be Function of K, Q such that

       A53: for x be object st x in K holds Pk[x, (k . x)] from FUNCT_2:sch 1( A44);

      defpred Pj[ object, object] means ex S be set st S = $1 & $2 in S;

      

       A54: for x be object st x in ( rng k) holds ex y be object st y in RAT & Pj[x, y]

      proof

        let x be object such that

         A55: x in ( rng k);

        x in Q by A55;

        then

        consider p,r be Real such that

         A56: x = [.p, r.[ and

         A57: r > p;

        reconsider xx = x as set by TARSKI: 1;

        consider y be Rational such that

         A58: y in xx by A56, A57, Lm4;

        take y;

        thus y in RAT by RAT_1:def 2;

        take xx;

        thus thesis by A58;

      end;

      consider j be Function of ( rng k), RAT such that

       A59: for x be object st x in ( rng k) holds Pj[x, (j . x)] from FUNCT_2:sch 1( A54);

      

       A60: for x,y be Element of S st x in K & y in K & x <> y holds (k . x) misses (k . y)

      proof

        let x,y be Element of S such that

         A61: x in K and

         A62: y in K and

         A63: x <> y;

        

         A64: Pk[x, (k . x)] & Pk[y, (k . y)] by A53, A61, A62;

        

         A65: (g . x) in U & (g . y) in U by A3, A61, A62, FUNCT_2: 5;

        thus ((k . x) /\ (k . y)) = {}

        proof

          assume not ((k . x) /\ (k . y)) = {} ;

          then

          consider l be object such that

           A66: l in ((k . x) /\ (k . y)) by XBOOLE_0: 7;

          

           A67: l in (k . x) & l in (k . y) by XBOOLE_0:def 4, A66;

           Pk[x, (k . x)] by A53, A61;

          then

          consider x1,rx be Real such that

           A68: x = x1 and

           A69: (k . x) = [.x1, rx.[;

           Pk[y, (k . y)] by A53, A62;

          then

          consider y1,ry be Real such that

           A70: y = y1 and

           A71: (k . y) = [.y1, ry.[;

          reconsider l as Real by A69, A66;

          

           A72: x1 <= l & l < rx by A69, A67, XXREAL_1: 3;

          

           A73: y1 <= l & l < ry by A71, A67, XXREAL_1: 3;

          per cases by A63, XXREAL_0: 1, A68, A70;

            suppose

             A74: x1 < y1;

            y1 < rx by A72, A73, XXREAL_0: 2;

            then

             A75: y1 in ].x1, rx.[ by XXREAL_1: 4, A74;

            reconsider Y = ].x1, rx.[ as Subset of R^1 by TOPMETR: 17;

            Y c= (k . x) by XXREAL_1: 22, A69;

            then

             A76: Y c= (g . x) by A64, XBOOLE_1: 1;

            reconsider gx = (g . x) as Subset of R^1 by TOPGEN_3:def 2, TOPMETR: 17, A65;

            

             A77: y in ( Int gx) by A76, BORSUK_5: 40, A70, A75, TOPS_1: 22;

            ( Int gx) in V by A65;

            then y in ( union V) by A77, TARSKI:def 4;

            hence contradiction by A62, XBOOLE_0:def 5;

          end;

            suppose

             A78: x1 > y1;

            x1 < ry by A72, A73, XXREAL_0: 2;

            then

             A79: x1 in ].y1, ry.[ by XXREAL_1: 4, A78;

            reconsider X = ].y1, ry.[ as Subset of R^1 by TOPMETR: 17;

            X c= (k . y) by XXREAL_1: 22, A71;

            then

             A80: X c= (g . y) by A64, XBOOLE_1: 1;

            reconsider gy = (g . y) as Subset of R^1 by A65, TOPGEN_3:def 2, TOPMETR: 17;

            

             A81: x in ( Int gy) by A80, BORSUK_5: 40, A68, A79, TOPS_1: 22;

            ( Int gy) in V by A65;

            then x in ( union V) by A81, TARSKI:def 4;

            hence contradiction by A61, XBOOLE_0:def 5;

          end;

        end;

      end;

      

       A82: ( rng j) c= RAT ;

      

       A83: ( dom j) = ( rng k) by FUNCT_2:def 1;

      

       A84: j is one-to-one

      proof

        let x1,x2 be object such that

         A85: x1 in ( dom j) and

         A86: x2 in ( dom j) and

         A87: (j . x1) = (j . x2);

        reconsider x1, x2 as set by TARSKI: 1;

        consider y1 be object such that

         A88: y1 in ( dom k) & x1 = (k . y1) by FUNCT_1:def 3, A85;

        consider y2 be object such that

         A89: y2 in ( dom k) & x2 = (k . y2) by FUNCT_1:def 3, A86;

        

         A90: y1 in K & y2 in K by A88, A89;

         Pj[x1, (j . x1)] & Pj[x2, (j . x2)] by A85, A86, A59;

        then ((k . y1) /\ (k . y2)) <> {} by A88, A89, XBOOLE_0:def 4, A87;

        hence thesis by A88, A89, A60, A90, XBOOLE_0:def 7;

      end;

      

       A91: ( card ( rng k)) c= omega by TOPGEN_3: 17, CARD_1: 10, A82, A83, A84;

      

       A92: [.1, 2.[ in Q;

      then

       A93: ( dom k) = K by FUNCT_2:def 1;

      

       A94: k is one-to-one

      proof

        let x1,x2 be object such that

         A95: x1 in ( dom k) and

         A96: x2 in ( dom k) and

         A97: (k . x1) = (k . x2);

        

         A98: x1 in K & x2 in K by A95, A96;

        (k . x1) in ( rng k) & (k . x2) in ( rng k) by A92, A95, A96, FUNCT_2: 4;

        then

         A99: (k . x1) in Q & (k . x2) in Q;

        consider p1,r1 be Real such that

         A100: (k . x1) = [.p1, r1.[ and

         A101: r1 > p1 by A99;

        consider q be Rational such that

         A102: q in (k . x1) by A100, A101, Lm4;

        q in ((k . x1) /\ (k . x2)) by A102, A97;

        hence x1 = x2 by A60, XBOOLE_0:def 7, A98;

      end;

      

       A103: ( card K) c= ( card ( rng k)) by CARD_1: 10, A93, A94;

      

       A104: ( card K) c= omega by A103, A91, XBOOLE_1: 1;

      ( dom g) = K by FUNCT_2:def 1, A3;

      then ( card ( rng g)) c= ( card K) by CARD_1: 12;

      then

       A105: ( rng g) is countable by CARD_3:def 14, A104, XBOOLE_1: 1;

      reconsider Z = ( rng g) as Subset-Family of S by TOPS_2: 2;

      

       A106: Z is Cover of K

      proof

        let x be object;

        assume

         A107: x in K;

        then

         A108: Pg[x, (g . x)] by A43;

        x in ( dom g) by A107, FUNCT_2:def 1, A3;

        then (g . x) in Z by FUNCT_1:def 3;

        hence x in ( union Z) by TARSKI:def 4, A108;

      end;

      W c= ( [#] S)

      proof

        let x be object;

        assume x in W;

        then x in ( [#] R^1 );

        hence x in ( [#] S) by TOPMETR: 17, TOPGEN_3:def 2;

      end;

      then

       A109: (W \/ K) = ( [#] S) by XBOOLE_1: 45;

      

       A110: (Z \/ Y) is Cover of ( [#] S)

      proof

        let x be object;

        assume x in ( [#] S);

        then x in W or x in K by XBOOLE_0:def 3, A109;

        then x in ( union Y) or x in ( union Z) by A31, A106, TARSKI:def 3, SETFAM_1:def 11;

        then x in (( union Y) \/ ( union Z)) by XBOOLE_0:def 3;

        hence x in ( union (Z \/ Y)) by ZFMISC_1: 78;

      end;

      reconsider G = (Z \/ Y) as Subset-Family of S;

      take G;

      thus G c= U by XBOOLE_1: 8;

      thus G is Cover of S by A110;

      thus G is countable by CARD_2: 85, A105, A39;

    end;

    registration

      cluster Sorgenfrey-line -> Lindelof;

      coherence by Lm9;

    end

    definition

      :: TOPGEN_6:def1

      func Sorgenfrey-plane -> non empty strict TopSpace equals [: Sorgenfrey-line , Sorgenfrey-line :];

      correctness ;

    end

    definition

      :: TOPGEN_6:def2

      func real-anti-diagonal -> Subset of [: REAL , REAL :] equals { [x, y] where x,y be Real : y = ( - x) };

      correctness

      proof

        set L = { [x, y] where x,y be Real : y = ( - x) };

        L c= [: REAL , REAL :]

        proof

          let z be object;

          assume z in L;

          then

          consider x,y be Real such that

           A1: z = [x, y] and y = ( - x);

          x in REAL & y in REAL by XREAL_0:def 1;

          hence z in [: REAL , REAL :] by A1, ZFMISC_1: 87;

        end;

        hence L is Subset of [: REAL , REAL :];

      end;

    end

    theorem :: TOPGEN_6:2

    

     Th2: [: RAT , RAT :] is dense Subset of Sorgenfrey-plane

    proof

       [: RAT , RAT :] c= ( [#] Sorgenfrey-plane )

      proof

        let z be object;

        assume z in [: RAT , RAT :];

        then

        consider x,y be object such that

         A1: x in RAT & y in RAT and

         A2: z = [x, y] by ZFMISC_1:def 2;

        x in REAL & y in REAL by A1, NUMBERS: 12;

        then x in ( [#] Sorgenfrey-line ) & y in ( [#] Sorgenfrey-line ) by TOPGEN_3:def 2;

        then z in [:( [#] Sorgenfrey-line ), ( [#] Sorgenfrey-line ):] by A2, ZFMISC_1:def 2;

        hence z in ( [#] Sorgenfrey-plane );

      end;

      then

      reconsider C = [: RAT , RAT :] as Subset of Sorgenfrey-plane ;

      for A be Subset of Sorgenfrey-plane st A <> {} & A is open holds A meets C

      proof

        let A be Subset of Sorgenfrey-plane such that

         A3: A <> {} and

         A4: A is open;

        consider B be Subset-Family of Sorgenfrey-plane such that

         A5: A = ( union B) and

         A6: (for e be set st e in B holds ex X1 be Subset of Sorgenfrey-line , Y1 be Subset of Sorgenfrey-line st (e = [:X1, Y1:] & X1 is open & Y1 is open)) by BORSUK_1: 5, A4;

        now

          assume

           A7: for e be set st e in B holds e = {} ;

          ( union B) c= {}

          proof

            let z be object;

            assume z in ( union B);

            then

            consider y be set such that

             A8: z in y & y in B by TARSKI:def 4;

            thus z in {} by A8, A7;

          end;

          hence contradiction by A5, A3;

        end;

        then

        consider e be set such that

         A9: e in B & e <> {} ;

        consider X1,Y1 be Subset of Sorgenfrey-line such that

         A10: e = [:X1, Y1:] and

         A11: X1 is open & Y1 is open by A6, A9;

        

         A12: X1 <> {} & Y1 <> {} by ZFMISC_1: 90, A9, A10;

        consider x1 be object such that

         A13: x1 in X1 by A12, XBOOLE_0: 7;

        consider y1 be object such that

         A14: y1 in Y1 by A12, XBOOLE_0: 7;

        consider ax be Subset of Sorgenfrey-line such that

         A15: ax in BB and x1 in ax and

         A16: ax c= X1 by YELLOW_9: 31, A11, A13, Lm8;

        consider ay be Subset of Sorgenfrey-line such that

         A17: ay in BB and y1 in ay and

         A18: ay c= Y1 by YELLOW_9: 31, A11, A14, Lm8;

        consider px,qx be Real such that

         A19: ax = [.px, qx.[ and

         A20: px < qx & qx is rational by A15, Lm7;

        consider py,qy be Real such that

         A21: ay = [.py, qy.[ and

         A22: py < qy & qy is rational by A17, Lm7;

        consider rx be Rational such that

         A23: px < rx & rx < qx by RAT_1: 7, A20;

        

         A24: rx in ax by A23, XXREAL_1: 3, A19;

        consider ry be Rational such that

         A25: py < ry & ry < qy by RAT_1: 7, A22;

        

         A26: ry in ay by A25, XXREAL_1: 3, A21;

        rx in RAT & ry in RAT by RAT_1:def 2;

        then

         A27: [rx, ry] in C by ZFMISC_1:def 2;

         [rx, ry] in [:X1, Y1:] by A24, A26, A16, A18, ZFMISC_1:def 2;

        then

         A28: [rx, ry] in A by A5, A9, A10, TARSKI:def 4;

        thus A meets C by A27, A28, XBOOLE_0: 3;

      end;

      hence [: RAT , RAT :] is dense Subset of Sorgenfrey-plane by TOPS_1: 45;

    end;

    theorem :: TOPGEN_6:3

    

     Th3: ( card real-anti-diagonal ) = continuum

    proof

      ( REAL , real-anti-diagonal ) are_equipotent

      proof

        defpred P[ object, object] means ex x be Real st $1 = x & $2 = [x, ( - x)];

        

         A1: for r be object st r in REAL holds ex a be object st a in real-anti-diagonal & P[r, a]

        proof

          let r be object;

          assume r in REAL ;

          then

          reconsider r as Real;

          set a = [r, ( - r)];

          a in real-anti-diagonal ;

          hence thesis;

        end;

        consider Z be Function of REAL , real-anti-diagonal such that

         A2: for r be object st r in REAL holds P[r, (Z . r)] from FUNCT_2:sch 1( A1);

        take Z;

        

         A3: real-anti-diagonal <> {}

        proof

          reconsider x = 1, y = ( - 1) as Element of REAL by XREAL_0:def 1;

          set z = [x, y];

          z in real-anti-diagonal ;

          hence real-anti-diagonal <> {} ;

        end;

        thus Z is one-to-one

        proof

          let r1,r2 be object such that

           A4: r1 in ( dom Z) & r2 in ( dom Z) and

           A5: (Z . r1) = (Z . r2);

          consider x1 be Real such that

           A6: r1 = x1 & (Z . r1) = [x1, ( - x1)] by A2, A4;

          consider x2 be Real such that

           A7: r2 = x2 & (Z . r2) = [x2, ( - x2)] by A2, A4;

          thus r1 = r2 by A6, A7, A5, XTUPLE_0: 1;

        end;

        thus ( dom Z) = REAL by A3, FUNCT_2:def 1;

        thus ( rng Z) = real-anti-diagonal

        proof

          thus ( rng Z) c= real-anti-diagonal ;

          thus real-anti-diagonal c= ( rng Z)

          proof

            let z be object;

            assume z in real-anti-diagonal ;

            then

            consider x,y be Real such that

             A8: z = [x, y] and

             A9: y = ( - x);

            consider x1 be Real such that

             A10: x = x1 & (Z . x) = [x1, ( - x1)] by A2, XREAL_0:def 1;

            thus z in ( rng Z) by A10, A8, A9, FUNCT_2: 4, A3, XREAL_0:def 1;

          end;

        end;

      end;

      hence ( card real-anti-diagonal ) = continuum by TOPGEN_3:def 4, CARD_1: 5;

    end;

    theorem :: TOPGEN_6:4

    

     Th4: real-anti-diagonal is closed Subset of Sorgenfrey-plane

    proof

      set L = real-anti-diagonal ;

      set S2 = Sorgenfrey-plane ;

      

       A1: L c= ( [#] S2)

      proof

        let z be object;

        assume z in L;

        then

        consider x,y be Real such that

         A2: z = [x, y] and y = ( - x);

        x in REAL & y in REAL by XREAL_0:def 1;

        then x in ( [#] Sorgenfrey-line ) & y in ( [#] Sorgenfrey-line ) by TOPGEN_3:def 2;

        then [x, y] in [:( [#] Sorgenfrey-line ), ( [#] Sorgenfrey-line ):] by ZFMISC_1:def 2;

        hence z in ( [#] Sorgenfrey-plane ) by A2;

      end;

      reconsider L = real-anti-diagonal as Subset of Sorgenfrey-plane by A1;

      defpred Pf[ object, object] means ex x,y be Real st $1 = [x, y] & $2 = (x + y);

      

       A3: for z be object st z in the carrier of S2 holds ex u be object st u in the carrier of R^1 & Pf[z, u]

      proof

        let z be object;

        assume z in the carrier of S2;

        then z in [:the carrier of Sorgenfrey-line , the carrier of Sorgenfrey-line :] by BORSUK_1:def 2;

        then

        consider x,y be object such that

         A4: x in the carrier of Sorgenfrey-line and

         A5: y in the carrier of Sorgenfrey-line and

         A6: z = [x, y] by ZFMISC_1:def 2;

        reconsider x as Element of REAL by A4, TOPGEN_3:def 2;

        reconsider y as Element of REAL by A5, TOPGEN_3:def 2;

        set u = (x + y);

        u in the carrier of R^1 by TOPMETR: 17;

        hence thesis by A6;

      end;

      consider f be Function of S2, R^1 such that

       A7: for z be object st z in the carrier of S2 holds Pf[z, (f . z)] from FUNCT_2:sch 1( A3);

      

       A8: for x,y be Element of REAL st [x, y] in the carrier of S2 holds (f . [x, y]) = (x + y)

      proof

        let x,y be Element of REAL such that

         A9: [x, y] in the carrier of S2;

        consider x1,y1 be Real such that

         A10: [x, y] = [x1, y1] & (f . [x, y]) = (x1 + y1) by A9, A7;

        x = x1 & y = y1 by A10, XTUPLE_0: 1;

        hence thesis by A10;

      end;

      for p be Point of S2, r be positive Real holds ex W be open Subset of S2 st p in W & (f .: W) c= ].((f . p) - r), ((f . p) + r).[

      proof

        let p be Point of S2;

        let r be positive Real;

        p in ( [#] S2);

        then p in [:the carrier of Sorgenfrey-line , the carrier of Sorgenfrey-line :] by BORSUK_1:def 2;

        then

        consider x,y be object such that

         A11: x in the carrier of Sorgenfrey-line and

         A12: y in the carrier of Sorgenfrey-line and

         A13: p = [x, y] by ZFMISC_1:def 2;

        reconsider x as Element of REAL by A11, TOPGEN_3:def 2;

        reconsider y as Element of REAL by A12, TOPGEN_3:def 2;

        

         A14: (f . p) = (x + y) by A13, A8;

        set U = ].((f . p) - r), ((f . p) + r).[;

        set W = [: [.x, (x + (r / 2)).[, [.y, (y + (r / 2)).[:];

        

         A15: W c= ( [#] S2)

        proof

          let z be object;

          assume z in W;

          then

          consider u,v be object such that

           A16: u in [.x, (x + (r / 2)).[ & v in [.y, (y + (r / 2)).[ and

           A17: z = [u, v] by ZFMISC_1:def 2;

          reconsider u, v as Element of ( [#] Sorgenfrey-line ) by A16, TOPGEN_3:def 2;

          u in ( [#] Sorgenfrey-line ) & v in ( [#] Sorgenfrey-line );

          then z in [:( [#] Sorgenfrey-line ), ( [#] Sorgenfrey-line ):] by A17, ZFMISC_1:def 2;

          hence z in ( [#] S2);

        end;

        reconsider W as Subset of S2 by A15;

        reconsider X = [.x, (x + (r / 2)).[ as Subset of Sorgenfrey-line by TOPGEN_3:def 2;

        reconsider Y = [.y, (y + (r / 2)).[ as Subset of Sorgenfrey-line by TOPGEN_3:def 2;

        X is open & Y is open by TOPGEN_3: 11;

        then

         A18: W is open by BORSUK_1: 6;

        (r / 2) is positive;

        then x < (x + (r / 2)) & y < (y + (r / 2)) by XREAL_1: 29;

        then x in [.x, (x + (r / 2)).[ & y in [.y, (y + (r / 2)).[ by XXREAL_1: 3;

        then

         A19: p in W by A13, ZFMISC_1:def 2;

        (f .: W) c= U

        proof

          let z be object;

          assume z in (f .: W);

          then

          consider w be object such that w in ( dom f) and

           A20: w in W and

           A21: z = (f . w) by FUNCT_1:def 6;

          consider x1,y1 be object such that

           A22: x1 in X & y1 in Y and

           A23: w = [x1, y1] by A20, ZFMISC_1:def 2;

          reconsider x1 as Element of REAL by A22;

          reconsider y1 as Element of REAL by A22;

          

           A24: x <= x1 & x1 < (x + (r / 2)) & y <= y1 & y1 < (y + (r / 2)) by A22, XXREAL_1: 3;

          

           A25: (x + y) <= (x1 + y1) by XREAL_1: 7, A24;

          ((x + y) - r) < (x + y) by XREAL_1: 44, XXREAL_0:def 6;

          then

           A26: ((x + y) - r) < (x1 + y1) by A25, XXREAL_0: 2;

          (x1 + y1) < ((x + (r / 2)) + (y + (r / 2))) by XREAL_1: 8, A24;

          then (x1 + y1) in U by A26, A14, XXREAL_1: 4;

          hence z in U by A23, A8, A20, A21;

        end;

        hence thesis by A19, A18;

      end;

      then

       A27: f is continuous by TOPS_4: 21;

      reconsider zz = 0 as Element of REAL by XREAL_0:def 1;

      reconsider k = {zz} as Subset of R^1 by TOPMETR: 17;

      reconsider k1 = [.zz, zz.] as Subset of R^1 by TOPMETR: 17;

      

       A28: k = k1 by XXREAL_1: 17;

      L = (f " k)

      proof

        hereby

          let z be object;

          assume

           A29: z in L;

          then

          consider x,y be Real such that

           A30: z = [x, y] and

           A31: y = ( - x);

          reconsider x, y as Element of REAL by XREAL_0:def 1;

          (f . z) = (x + y) by A8, A30, A29;

          then (f . z) in k by TARSKI:def 1, A31;

          hence z in (f " k) by FUNCT_2: 38, A29;

        end;

        let z be object;

        assume z in (f " k);

        then

         A32: z in ( [#] S2) & (f . z) in k by FUNCT_2: 38;

        then

         A33: z in [:the carrier of Sorgenfrey-line , the carrier of Sorgenfrey-line :] by BORSUK_1:def 2;

        consider x,y be object such that

         A34: x in the carrier of Sorgenfrey-line and

         A35: y in the carrier of Sorgenfrey-line and

         A36: z = [x, y] by A33, ZFMISC_1:def 2;

        reconsider x1 = x as Element of REAL by A34, TOPGEN_3:def 2;

        reconsider y1 = y as Element of REAL by A35, TOPGEN_3:def 2;

        (f . z) = (x1 + y1) by A8, A36, A32;

        then (x1 + y1) = 0 by A32, TARSKI:def 1;

        then ( - x1) = y1;

        hence z in L by A36;

      end;

      hence thesis by A28, A27, TREAL_1: 1;

    end;

    the carrier of Sorgenfrey-line = REAL by TOPGEN_3:def 2;

    then

     Lm10: the carrier of Sorgenfrey-plane = [: REAL , REAL :] by BORSUK_1:def 2;

    

     Lm11: for x,y be Real st [x, y] in real-anti-diagonal holds y = ( - x)

    proof

      let x,y be Real;

      assume [x, y] in real-anti-diagonal ;

      then

      consider x1,y1 be Real such that

       A1: [x, y] = [x1, y1] and

       A2: y1 = ( - x1);

      x = x1 & y = y1 by A1, XTUPLE_0: 1;

      hence y = ( - x) by A2;

    end;

    theorem :: TOPGEN_6:5

    

     Th5: for A be Subset of Sorgenfrey-plane st A = real-anti-diagonal holds ( Der A) is empty

    proof

      let A be Subset of Sorgenfrey-plane such that

       A1: A = real-anti-diagonal ;

      assume not ( Der A) is empty;

      then

      consider a be object such that

       A2: a in ( Der A) by XBOOLE_0: 7;

      a is_an_accumulation_point_of A by TOPGEN_1:def 3, A2;

      then

       A3: a in ( Cl (A \ {a})) by TOPGEN_1:def 2;

      consider x,y be object such that

       A4: x in REAL & y in REAL and

       A5: a = [x, y] by ZFMISC_1:def 2, Lm10, A2;

      reconsider x, y as Real by A4;

      per cases ;

        suppose

         A6: y >= ( - x);

        set Gx = [.x, (x + 1).[;

        set Gy = [.y, (y + 1).[;

        reconsider Gx, Gy as Subset of Sorgenfrey-line by TOPGEN_3:def 2;

        set G = [:Gx, Gy:];

        reconsider G as Subset of Sorgenfrey-plane ;

        Gx is open & Gy is open by TOPGEN_3: 11;

        then

         A7: G is open by BORSUK_1: 6;

        x <= x & x < (x + 1) by XREAL_1: 29;

        then

         A8: x in Gx by XXREAL_1: 3;

        y <= y & y < (y + 1) by XREAL_1: 29;

        then y in Gy by XXREAL_1: 3;

        then

         A9: a in G by A5, A8, ZFMISC_1:def 2;

        now

          assume (G /\ (A \ {a})) <> {} ;

          then

          consider z be object such that

           A10: z in (G /\ (A \ {a})) by XBOOLE_0:def 1;

          z in G & z in (A \ {a}) by XBOOLE_0:def 4, A10;

          then

           A11: z in G & z in A & not z in {a} by XBOOLE_0:def 5;

          consider xz,yz be object such that

           A12: xz in [.x, (x + 1).[ & yz in [.y, (y + 1).[ and

           A13: z = [xz, yz] by ZFMISC_1:def 2, A11;

          reconsider xz as Real by A12;

          reconsider yz as Real by A12;

          

           A14: x <= xz & y <= yz by A12, XXREAL_1: 3;

          

           A15: ( - x) >= ( - xz) & y <= ( - xz) by A14, Lm11, A1, A11, A13, XREAL_1: 24;

          

           A16: ( - x) >= y by XXREAL_0: 2, A15;

          

           A17: ( - x) = y by A16, A6, XXREAL_0: 1;

          then

           A18: ( - x) <= yz by A12, XXREAL_1: 3;

          

           A19: ( - x) <= ( - xz) by Lm11, A1, A11, A13, A18;

          

           A20: x >= xz by XREAL_1: 24, A19;

          

           A21: x = xz by A20, A14, XXREAL_0: 1;

          then y = yz by A17, Lm11, A1, A11, A13;

          hence contradiction by A11, TARSKI:def 1, A13, A5, A21;

        end;

        then G misses (A \ {a}) by XBOOLE_0:def 7;

        hence contradiction by A7, A9, A3, PRE_TOPC:def 7;

      end;

        suppose

         A22: y < ( - x);

        set Gx = [.x, (x + ( |.(x + y).| / 2)).[;

        set Gy = [.y, (y + ( |.(x + y).| / 2)).[;

        reconsider Gx, Gy as Subset of Sorgenfrey-line by TOPGEN_3:def 2;

        reconsider G = [:Gx, Gy:] as Subset of Sorgenfrey-plane ;

        Gx is open & Gy is open by TOPGEN_3: 11;

        then

         A23: G is open by BORSUK_1: 6;

        

         A24: (y + x) < 0 by A22, XREAL_1: 61;

        

         A25: |.(x + y).| = ( - (x + y)) by ABSVALUE:def 1, A22, XREAL_1: 61;

        

         A26: |.(x + y).| > 0 by A24, A25, XREAL_1: 58;

        then x < (x + ( |.(x + y).| / 2)) by XREAL_1: 29, XREAL_1: 139;

        then

         A27: x in Gx by XXREAL_1: 3;

        y < (y + ( |.(x + y).| / 2)) by XREAL_1: 29, A26, XREAL_1: 139;

        then y in Gy by XXREAL_1: 3;

        then

         A28: a in G by A5, A27, ZFMISC_1:def 2;

        now

          assume (G /\ (A \ {a})) <> {} ;

          then

          consider z be object such that

           A29: z in (G /\ (A \ {a})) by XBOOLE_0:def 1;

          z in G & z in (A \ {a}) by A29, XBOOLE_0:def 4;

          then

           A30: z in G & z in A & not z in {a} by XBOOLE_0:def 5;

          consider xz,yz be object such that

           A31: xz in [.x, (x + ( |.(x + y).| / 2)).[ & yz in [.y, (y + ( |.(x + y).| / 2)).[ and

           A32: z = [xz, yz] by ZFMISC_1:def 2, A30;

          reconsider xz, yz as Real by A31;

          

           A33: yz = ( - xz) by Lm11, A1, A30, A32;

          

           A34: xz < (x + ( |.(x + y).| / 2)) & yz < (y + ( |.(x + y).| / 2)) by A31, XXREAL_1: 3;

          (xz + yz) < ((x + ( |.(x + y).| / 2)) + (y + ( |.(x + y).| / 2))) by A34, XREAL_1: 8;

          hence contradiction by A33, A25;

        end;

        then G misses (A \ {a}) by XBOOLE_0:def 7;

        hence contradiction by A23, A28, A3, PRE_TOPC:def 7;

      end;

    end;

    theorem :: TOPGEN_6:6

    

     Th6: for A be Subset of real-anti-diagonal holds A is closed Subset of Sorgenfrey-plane

    proof

      reconsider B = real-anti-diagonal as closed Subset of Sorgenfrey-plane by Th4;

      let A be Subset of real-anti-diagonal ;

      A c= B;

      then

      reconsider A as Subset of Sorgenfrey-plane by XBOOLE_1: 1;

      ( Der A) c= ( Der B) by TOPGEN_1: 30;

      then ( Der A) c= {} by Th5;

      then ( Der A) = {} ;

      then ( Cl A) = (A \/ {} ) by TOPGEN_1: 29;

      hence thesis;

    end;

    

     Lm12: not Sorgenfrey-plane is Lindelof

    proof

      set S2 = Sorgenfrey-plane ;

      reconsider L = real-anti-diagonal as Subset of S2 by Lm10;

      reconsider T = (S2 | L) as SubSpace of S2;

      

       A1: for v be Subset of T, z be set st v = {z} & z in L holds v is open

      proof

        let v be Subset of T, z be set such that

         A2: v = {z} and

         A3: z in L;

        consider x,y be Real such that

         A4: z = [x, y] and

         A5: y = ( - x) by A3;

        set Ux = [.x, (x + 1).[;

        reconsider Ux as open Subset of Sorgenfrey-line by TOPGEN_3: 11;

        set Uy = [.y, (y + 1).[;

        reconsider Uy as open Subset of Sorgenfrey-line by TOPGEN_3: 11;

        reconsider U2 = [:Ux, Uy:] as Subset of S2;

        

         A6: U2 in the topology of S2 by BORSUK_1: 6, PRE_TOPC:def 2;

        

         A7: (U2 /\ L) = v

        proof

          hereby

            let p be object;

            assume p in (U2 /\ L);

            then

             A8: p in U2 & p in L by XBOOLE_0:def 4;

            then

            consider p1,p2 be object such that

             A9: p1 in Ux & p2 in Uy and

             A10: p = [p1, p2] by ZFMISC_1:def 2;

            consider r1,r2 be Real such that

             A11: p = [r1, r2] and

             A12: r2 = ( - r1) by A8;

            p1 = r1 & p2 = r2 by XTUPLE_0: 1, A10, A11;

            then

             A13: r1 >= x & r1 < (x + 1) & r2 >= y & r2 < (y + 1) by XXREAL_1: 3, A9;

            then r1 <= x by XREAL_1: 24, A5, A12;

            then

             A14: r1 = x by A13, XXREAL_0: 1;

            r2 <= y by XREAL_1: 24, A12, A13, A5;

            then r2 = y by A13, XXREAL_0: 1;

            hence p in v by A2, A14, A11, A4, TARSKI:def 1;

          end;

          let p be object;

          assume p in v;

          then

           A15: p = z by A2, TARSKI:def 1;

          x < (x + 1) & y < (y + 1) by XREAL_1: 29;

          then x in Ux & y in Uy by XXREAL_1: 3;

          then p in U2 by ZFMISC_1:def 2, A15, A4;

          hence p in (U2 /\ L) by XBOOLE_0:def 4, A15, A3;

        end;

        L = ( [#] T) by PRE_TOPC:def 5;

        hence v is open by A6, A7, PRE_TOPC:def 4;

      end;

      set V = { {v} where v be Element of S2 : v in L };

      V c= ( bool ( [#] T))

      proof

        let z be object;

        reconsider zz = z as set by TARSKI: 1;

        assume z in V;

        then

        consider v be Element of S2 such that

         A16: z = {v} and

         A17: v in L;

        

         A18: v in ( [#] T) by A17, PRE_TOPC:def 5;

        zz c= ( [#] T)

        proof

          let y be object;

          assume y in zz;

          hence y in ( [#] T) by TARSKI:def 1, A16, A18;

        end;

        hence z in ( bool ( [#] T));

      end;

      then

      reconsider V as Subset-Family of T;

      

       A19: V is open

      proof

        let u be Subset of T;

        assume u in V;

        then

        consider z be Element of S2 such that

         A20: u = {z} and

         A21: z in L;

        thus u is open by A20, A21, A1;

      end;

      

       A22: V is Cover of T

      proof

        let z be object;

        assume z in the carrier of T;

        then z in ( [#] T);

        then z in L by PRE_TOPC:def 5;

        then {z} in V & z in {z} by TARSKI:def 1;

        hence z in ( union V) by TARSKI:def 4;

      end;

      defpred Pg[ object, object] means ex x,y be Real st $1 = x & $2 = { [x, y]};

      

       A23: for r be object st r in REAL holds ex v be object st v in V & Pg[r, v]

      proof

        let r be object;

        assume r in REAL ;

        then

        reconsider r as Real;

        reconsider y = ( - r) as Real;

        set u = [r, y];

        

         A24: u in L;

        then

        reconsider u as Element of S2;

        set v = {u};

        v in V by A24;

        hence thesis;

      end;

      consider g be Function of REAL , V such that

       A25: for r be object st r in REAL holds Pg[r, (g . r)] from FUNCT_2:sch 1( A23);

      reconsider x = 1 as Element of REAL by XREAL_0:def 1;

      reconsider y = ( - 1) as Element of REAL by XREAL_0:def 1;

      set z = [x, y];

      

       A26: z in L;

      then

      reconsider z as Element of S2;

       {z} in V by A26;

      then

       A27: ( dom g) = REAL by FUNCT_2:def 1;

      

       A28: g is one-to-one

      proof

        let r1,r2 be object such that

         A29: r1 in ( dom g) and

         A30: r2 in ( dom g) and

         A31: (g . r1) = (g . r2);

        consider x1,y1 be Real such that

         A32: r1 = x1 and

         A33: (g . r1) = { [x1, y1]} by A25, A29;

        consider x2,y2 be Real such that

         A34: r2 = x2 and

         A35: (g . r2) = { [x2, y2]} by A25, A30;

         [x1, y1] = [x2, y2] by ZFMISC_1: 3, A35, A33, A31;

        hence r1 = r2 by A32, A34, XTUPLE_0: 1;

      end;

      ( rng g) c= V;

      then

       A36: ( card REAL ) c= ( card V) by CARD_1: 10, A28, A27;

      

       A37: not ( card V) c= omega by A36, TOPGEN_3: 30, TOPGEN_3:def 4;

      

       A38: not ex G be Subset-Family of T st G c= V & G is Cover of T & G is countable

      proof

        assume ex G be Subset-Family of T st G c= V & G is Cover of T & G is countable;

        then

        consider G be Subset-Family of T such that

         A39: G c= V and

         A40: G is Cover of T and

         A41: G is countable;

        per cases by A39, XBOOLE_0:def 8;

          suppose G c< V;

          then

          consider u be object such that

           A42: u in V and

           A43: not u in G by XBOOLE_0: 6;

          consider v be Element of S2 such that

           A44: u = {v} and

           A45: v in L by A42;

          

           A46: ( [#] T) c= ( union G) by SETFAM_1:def 11, A40;

          v in ( [#] T) by A45, PRE_TOPC:def 5;

          then

          consider u1 be set such that

           A47: v in u1 and

           A48: u1 in G by TARSKI:def 4, A46;

          u1 in V by A39, A48;

          then

          consider v1 be Element of S2 such that

           A49: u1 = {v1} and v1 in L;

          thus contradiction by A43, A44, A49, A48, A47, TARSKI:def 1;

        end;

          suppose G = V;

          hence contradiction by A37, CARD_3:def 14, A41;

        end;

      end;

      thus not S2 is Lindelof by Th4, METRIZTS:def 2, A19, A22, A38;

    end;

    registration

      cluster Sorgenfrey-plane -> non Lindelof;

      coherence by Lm12;

    end

    registration

      cluster Sorgenfrey-line -> regular;

      coherence by TOPGEN_5: 59;

    end

    registration

      cluster Sorgenfrey-line -> normal;

      coherence ;

    end

    

     Lm13: not Sorgenfrey-plane is normal

    proof

      set L = real-anti-diagonal ;

      set S2 = Sorgenfrey-plane ;

      reconsider C = [: RAT , RAT :] as dense Subset of Sorgenfrey-plane by Th2;

      defpred P[ object, object] means ex S be set, U,V be open Subset of S2 st $1 = S & $2 = (U /\ C) & S c= U & (L \ S) c= V & U misses V;

      

       A1: ( exp (2, omega )) in ( exp (2,( exp (2, omega )))) by CARD_5: 14;

      ( card C) c= omega by CARD_3:def 14, CARD_4: 7;

      then

       A2: ( exp (2,( card C))) c= ( exp (2, omega )) by CARD_2: 93;

      assume

       A3: for W,V be Subset of S2 st W <> {} & V <> {} & W is closed & V is closed & W misses V holds ex P,Q be Subset of S2 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 L) holds ex b be object st P[a, b]

      proof

        let a be object;

        assume a in ( bool L);

        then

        reconsider aa = a as Subset of L;

        reconsider a9 = (L \ aa) as Subset of L by XBOOLE_1: 36;

        reconsider A = aa, B = a9 as closed Subset of S2 by Th6;

        per cases ;

          suppose

           A5: a = {} ;

          take {} , {} ;

          take ( {} S2), ( [#] S2);

          thus thesis by A5, Th4, XBOOLE_1: 65;

        end;

          suppose

           A6: a = L;

          take (( [#] S2) /\ C), L;

          take ( [#] S2), ( {} S2);

          thus thesis by A6, Th4, XBOOLE_1: 37, XBOOLE_1: 65;

        end;

          suppose

           A7: a <> {} & a <> L;

          ((aa ` ) ` ) = (a9 ` );

          then

           A8: B <> ( {} L) by A7;

          A misses B by XBOOLE_1: 79;

          then

          consider P,Q be Subset of S2 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 L) and

       A15: for a be object st a in ( bool L) 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 L 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;

         P[B, (G . B)] by A15;

        then

        consider UB,VB be open Subset of S2 such that

         A22: (G . B) = (UB /\ C) and

         A23: B c= UB and

         A24: (L \ B) c= VB and

         A25: UB misses VB;

         P[A, (G . A)] by A15;

        then

        consider UA,VA be open Subset of S2 such that

         A26: (G . A) = (UA /\ C) and

         A27: A c= UA and

         A28: (L \ A) c= VA and

         A29: UA misses VA;

        (B \ A) = (B /\ (A ` )) by SUBSET_1: 13;

        then

         A30: (B \ A) c= (UB /\ VA) by A28, A23, XBOOLE_1: 27;

        (A \ B) = (A /\ (B ` )) by SUBSET_1: 13;

        then (A \ B) c= (UA /\ VB) by A27, A24, XBOOLE_1: 27;

        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, A30, A21, TOPS_1: 45;

        then

        consider z be set such that

         A31: z in C and

         A32: z in (UA /\ VB) or z in (UB /\ VA);

        z in UA & z in VB or z in UB & z in VA by A32, XBOOLE_0:def 4;

        then z in UA & not z in UB or z in UB & not z in UA by A29, A25, XBOOLE_0: 3;

        then z in (G . A) & not z in (G . B) or z in (G . B) & not z in (G . A) by A26, A22, A31, XBOOLE_0:def 4;

        hence thesis by A18;

      end;

      then

       A33: ( 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

         A34: b in ( dom G) and

         A35: a = (G . b) by FUNCT_1:def 3;

         P[b, a] by A14, A15, A34, A35;

        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 L)) c= ( card ( bool C)) by A33, A14, XBOOLE_1: 1;

      then

       A36: ( exp (2, continuum )) c= ( card ( bool C)) by CARD_2: 31, Th3;

      ( card ( bool C)) = ( exp (2,( card C))) by CARD_2: 31;

      then ( exp (2, continuum )) c= ( exp (2, omega )) by A36, A2, XBOOLE_1: 1;

      then ( exp (2, omega )) in ( exp (2, omega )) by A1, TOPGEN_3: 29;

      hence contradiction;

    end;

    registration

      cluster Sorgenfrey-plane -> non normal;

      coherence by Lm13;

    end