waybel25.miz



    begin

    theorem :: WAYBEL25:1

    for p be Point of Sierpinski_Space st p = 0 holds {p} is closed

    proof

      set S = Sierpinski_Space ;

      let p be Point of S;

      

       A1: the carrier of S = { 0 , 1} by WAYBEL18:def 9;

      assume

       A2: p = 0 ;

      

       A3: (( [#] S) \ {p}) = {1}

      proof

        thus (( [#] S) \ {p}) c= {1}

        proof

          let a be object;

          assume

           A4: a in (( [#] S) \ {p});

          then not a in {p} by XBOOLE_0:def 5;

          then a <> 0 by A2, TARSKI:def 1;

          then a = 1 by A1, A4, TARSKI:def 2;

          hence thesis by TARSKI:def 1;

        end;

        let a be object;

        assume a in {1};

        then

         A5: a = 1 by TARSKI:def 1;

        then

         A6: not a in {p} by A2, TARSKI:def 1;

        a in ( [#] S) by A1, A5, TARSKI:def 2;

        hence thesis by A6, XBOOLE_0:def 5;

      end;

      the topology of S = { {} , {1}, { 0 , 1}} by WAYBEL18:def 9;

      hence (( [#] S) \ {p}) in the topology of S by A3, ENUMSET1:def 1;

    end;

    theorem :: WAYBEL25:2

    

     Th2: for p be Point of Sierpinski_Space st p = 1 holds {p} is non closed

    proof

      set S = Sierpinski_Space ;

      let p be Point of S;

      

       A1: the carrier of S = { 0 , 1} by WAYBEL18:def 9;

      assume

       A2: p = 1;

      

       A3: (( [#] S) \ {p}) = { 0 }

      proof

        thus (( [#] S) \ {p}) c= { 0 }

        proof

          let a be object;

          assume

           A4: a in (( [#] S) \ {p});

          then not a in {p} by XBOOLE_0:def 5;

          then a <> 1 by A2, TARSKI:def 1;

          then a = 0 by A1, A4, TARSKI:def 2;

          hence thesis by TARSKI:def 1;

        end;

        let a be object;

        assume a in { 0 };

        then

         A5: a = 0 by TARSKI:def 1;

        then

         A6: not a in {p} by A2, TARSKI:def 1;

        a in ( [#] S) by A1, A5, TARSKI:def 2;

        hence thesis by A6, XBOOLE_0:def 5;

      end;

      

       A7: { 0 } <> {1} by ZFMISC_1: 3;

      

       A8: { 0 } <> { 0 , 1} by ZFMISC_1: 5;

      the topology of S = { {} , {1}, { 0 , 1}} by WAYBEL18:def 9;

      hence not (( [#] S) \ {p}) in the topology of S by A7, A8, A3, ENUMSET1:def 1;

    end;

    registration

      cluster Sierpinski_Space -> non T_1;

      coherence

      proof

        set S = Sierpinski_Space ;

        ex p be Point of S st ( Cl {p}) <> {p}

        proof

          the carrier of S = { 0 , 1} by WAYBEL18:def 9;

          then

          reconsider p = 1 as Point of S by TARSKI:def 2;

          take p;

          thus thesis by Th2;

        end;

        hence thesis by YELLOW_8: 26;

      end;

    end

    registration

      cluster complete Scott -> T_0 for TopLattice;

      coherence by WAYBEL11: 10;

    end

    registration

      cluster injective strict for T_0-TopSpace;

      existence

      proof

        take Sierpinski_Space ;

        thus thesis;

      end;

    end

    registration

      cluster complete Scott strict for TopLattice;

      existence

      proof

        set T = the complete Scott strict TopLattice;

        take T;

        thus thesis;

      end;

    end

    theorem :: WAYBEL25:3

    

     Th3: for I be non empty set, T be Scott TopAugmentation of ( product (I --> ( BoolePoset { 0 }))) holds the carrier of T = the carrier of ( product (I --> Sierpinski_Space ))

    proof

      set S = Sierpinski_Space , B = ( BoolePoset { 0 });

      let I be non empty set, T be Scott TopAugmentation of ( product (I --> ( BoolePoset { 0 })));

      

       A1: ( dom ( Carrier (I --> B))) = I by PARTFUN1:def 2;

      

       A2: ( dom ( Carrier (I --> S))) = I by PARTFUN1:def 2;

      

       A3: for x be object st x in ( dom ( Carrier (I --> S))) holds (( Carrier (I --> B)) . x) = (( Carrier (I --> S)) . x)

      proof

        let x be object;

        assume

         A4: x in ( dom ( Carrier (I --> S)));

        then

         A5: ex T be 1-sorted st T = ((I --> S) . x) & (( Carrier (I --> S)) . x) = the carrier of T by PRALG_1:def 15;

        ex R be 1-sorted st R = ((I --> B) . x) & (( Carrier (I --> B)) . x) = the carrier of R by A4, PRALG_1:def 15;

        

        hence (( Carrier (I --> B)) . x) = the carrier of B by A4, FUNCOP_1: 7

        .= ( bool { 0 }) by WAYBEL_7: 2

        .= the carrier of S by WAYBEL18:def 9, YELLOW14: 1

        .= (( Carrier (I --> S)) . x) by A4, A5, FUNCOP_1: 7;

      end;

       the RelStr of T = the RelStr of ( product (I --> B)) by YELLOW_9:def 4;

      

      hence the carrier of T = ( product ( Carrier (I --> B))) by YELLOW_1:def 4

      .= ( product ( Carrier (I --> S))) by A1, A2, A3, FUNCT_1: 2

      .= the carrier of ( product (I --> S)) by WAYBEL18:def 3;

    end;

    theorem :: WAYBEL25:4

    

     Th4: for L1,L2 be complete LATTICE, T1 be Scott TopAugmentation of L1, T2 be Scott TopAugmentation of L2, h be Function of L1, L2, H be Function of T1, T2 st h = H & h is isomorphic holds H is being_homeomorphism

    proof

      let L1,L2 be complete LATTICE, T1 be Scott TopAugmentation of L1, T2 be Scott TopAugmentation of L2, h be Function of L1, L2, H be Function of T1, T2 such that

       A1: h = H and

       A2: h is isomorphic;

      

       A3: the RelStr of L2 = the RelStr of T2 by YELLOW_9:def 4;

      

       A4: the RelStr of L1 = the RelStr of T1 by YELLOW_9:def 4;

      then

      reconsider H9 = (h " ) as Function of T2, T1 by A3;

      consider g be Function of L2, L1 such that

       A5: g = (h " );

      g = (h qua Function " ) by A2, A5, TOPS_2:def 4;

      then g is isomorphic by A2, WAYBEL_0: 68;

      then

      reconsider h2 = (h " ) as sups-preserving Function of L2, L1 by A5, WAYBEL13: 20;

      

       A6: ( rng H) = ( [#] T2) by A1, A2, A3, WAYBEL_0: 66;

      

       A7: for x be object st x in ( dom H9) holds (H9 . x) = ((H " ) . x)

      proof

        let x be object;

        assume x in ( dom H9);

        

         A8: H is onto by A6, FUNCT_2:def 3;

        

        thus (H9 . x) = ((h qua Function " ) . x) by A2, TOPS_2:def 4

        .= ((H " ) . x) by A1, A2, A8, TOPS_2:def 4;

      end;

      h2 is directed-sups-preserving;

      then

       A9: H9 is directed-sups-preserving by A4, A3, WAYBEL21: 6;

      ( dom (H " )) = the carrier of T2 by FUNCT_2:def 1

      .= ( dom H9) by FUNCT_2:def 1;

      then

       A10: (H " ) = H9 by A7, FUNCT_1: 2;

      reconsider h1 = h as sups-preserving Function of L1, L2 by A2, WAYBEL13: 20;

      h1 is directed-sups-preserving;

      then

       A11: H is directed-sups-preserving by A1, A4, A3, WAYBEL21: 6;

      ( dom H) = ( [#] T1) by FUNCT_2:def 1;

      hence thesis by A1, A2, A11, A9, A6, A10;

    end;

    theorem :: WAYBEL25:5

    

     Th5: for L1,L2 be complete LATTICE, T1 be Scott TopAugmentation of L1, T2 be Scott TopAugmentation of L2 st (L1,L2) are_isomorphic holds (T1,T2) are_homeomorphic

    proof

      let L1,L2 be complete LATTICE, T1 be Scott TopAugmentation of L1, T2 be Scott TopAugmentation of L2;

      given h be Function of L1, L2 such that

       A1: h is isomorphic;

      

       A2: the RelStr of L2 = the RelStr of T2 by YELLOW_9:def 4;

       the RelStr of L1 = the RelStr of T1 by YELLOW_9:def 4;

      then

      reconsider H = h as Function of T1, T2 by A2;

      take H;

      thus thesis by A1, Th4;

    end;

    theorem :: WAYBEL25:6

    

     Th6: for S,T be non empty TopSpace st S is injective & (S,T) are_homeomorphic holds T is injective

    proof

      let S,T be non empty TopSpace such that

       A1: S is injective and

       A2: (S,T) are_homeomorphic ;

      consider p be Function of S, T such that

       A3: p is being_homeomorphism by A2;

      let X be non empty TopSpace, f be Function of X, T;

      assume

       A4: f is continuous;

      let Y be non empty TopSpace;

      assume

       A5: X is SubSpace of Y;

      then

       A6: ( [#] X) c= ( [#] Y) by PRE_TOPC:def 4;

      

       A7: p is one-to-one by A3;

      set F = ((p " ) * f);

      (p " ) is continuous by A3;

      then

      consider G be Function of Y, S such that

       A8: G is continuous and

       A9: (G | the carrier of X) = F by A1, A4, A5;

      take g = (p * G);

      

       A10: ( rng p) = ( [#] T) by A3;

      

       A11: for x be object st x in ( dom f) holds (g . x) = (f . x)

      proof

        let x be object;

        assume

         A12: x in ( dom f);

        then

         A13: (f . x) in ( rng f) by FUNCT_1:def 3;

        then (f . x) in the carrier of T;

        then

         A14: (f . x) in ( dom (p " )) by FUNCT_2:def 1;

        x in the carrier of X by A12;

        then x in the carrier of Y by A6;

        then x in ( dom G) by FUNCT_2:def 1;

        

        hence (g . x) = (p . (G . x)) by FUNCT_1: 13

        .= (p . (((p " ) * f) . x)) by A9, A12, FUNCT_1: 49

        .= (p . ((p " ) . (f . x))) by A12, FUNCT_1: 13

        .= ((p * (p " )) . (f . x)) by A14, FUNCT_1: 13

        .= (( id the carrier of T) . (f . x)) by A10, A7, TOPS_2: 52

        .= (f . x) by A13, FUNCT_1: 17;

      end;

      p is continuous by A3;

      hence g is continuous by A8;

      ( dom f) = the carrier of X by FUNCT_2:def 1

      .= (the carrier of Y /\ the carrier of X) by A6, XBOOLE_1: 28

      .= (( dom g) /\ the carrier of X) by FUNCT_2:def 1;

      hence thesis by A11, FUNCT_1: 46;

    end;

    theorem :: WAYBEL25:7

    for L1,L2 be complete LATTICE, T1 be Scott TopAugmentation of L1, T2 be Scott TopAugmentation of L2 st (L1,L2) are_isomorphic & T1 is injective holds T2 is injective by Th5, Th6;

    definition

      let X,Y be non empty TopSpace;

      :: original: is_Retract_of

      redefine

      :: WAYBEL25:def1

      pred X is_Retract_of Y means ex c be continuous Function of X, Y, r be continuous Function of Y, X st (r * c) = ( id X);

      compatibility

      proof

        thus X is_Retract_of Y implies ex c be continuous Function of X, Y, r be continuous Function of Y, X st (r * c) = ( id X)

        proof

          given f be Function of Y, Y such that

           A1: f is continuous and

           A2: (f * f) = f and

           A3: (( Image f),X) are_homeomorphic ;

          consider h be Function of ( Image f), X such that

           A4: h is being_homeomorphism by A3;

          

           A5: ( corestr f) is continuous by A1, WAYBEL18: 10;

          (h " ) is continuous by A4;

          then

          reconsider c = (( incl ( Image f)) * (h " )) as continuous Function of X, Y;

          h is continuous by A4;

          then

          reconsider r = (h * ( corestr f)) as continuous Function of Y, X by A5;

          take c, r;

          

           A6: ( rng h) = ( [#] X) by A4;

          

           A7: h is one-to-one by A4;

          

          thus (r * c) = (h * (( corestr f) * (( incl ( Image f)) * (h " )))) by RELAT_1: 36

          .= (h * ((( corestr f) * ( incl ( Image f))) * (h " ))) by RELAT_1: 36

          .= (h * (( id ( Image f)) * (h " ))) by A2, YELLOW14: 35

          .= (h * (h " )) by FUNCT_2: 17

          .= ( id X) by A6, A7, TOPS_2: 52;

        end;

        given c be continuous Function of X, Y, r be continuous Function of Y, X such that

         A8: (r * c) = ( id X);

        take f = (c * r);

        

         A9: ( dom c) = the carrier of X by FUNCT_2:def 1

        .= ( rng r) by A8, FUNCT_2: 18;

        then

        reconsider cf = ( corestr c) as Function of X, ( Image f) by RELAT_1: 28;

        

         A10: ( Image f) = ( Image c) by A9, RELAT_1: 28;

        the carrier of ( Image c) c= the carrier of Y by BORSUK_1: 1;

        then ( id ( Image c)) is Function of the carrier of ( Image c), the carrier of Y by FUNCT_2: 7;

        then

        reconsider q = (r * ( id ( Image c))) as Function of ( Image f), X by A10;

        

         A11: ( [#] X) <> {} ;

        

         A12: for P be Subset of X st P is open holds (q " P) is open

        proof

          let P be Subset of X;

          

           A13: ( dom ( id ( Image c))) = ( [#] ( Image c));

          

           A14: (( id ( Image c)) " (r " P)) = ((r " P) /\ ( [#] ( Image c)))

          proof

            thus (( id ( Image c)) " (r " P)) c= ((r " P) /\ ( [#] ( Image c)))

            proof

              let a be object;

              assume

               A15: a in (( id ( Image c)) " (r " P));

              then (( id ( Image c)) . a) in (r " P) by FUNCT_1:def 7;

              then a in (r " P) by A15, FUNCT_1: 18;

              hence thesis by A15, XBOOLE_0:def 4;

            end;

            let a be object;

            assume

             A16: a in ((r " P) /\ ( [#] ( Image c)));

            then a in (r " P) by XBOOLE_0:def 4;

            then (( id ( Image c)) . a) in (r " P) by A16, FUNCT_1: 18;

            hence thesis by A13, A16, FUNCT_1:def 7;

          end;

          assume P is open;

          then (r " P) is open by A11, TOPS_2: 43;

          then

           A17: (r " P) in the topology of Y;

          (q " P) = (( id ( Image c)) " (r " P)) by RELAT_1: 146;

          hence (q " P) in the topology of ( Image f) by A10, A17, A14, PRE_TOPC:def 4;

        end;

        

         A18: (r * (cf * (cf " ))) = (( id X) * (cf " )) by A8, RELAT_1: 36;

        thus f is continuous;

        

        thus (f * f) = (c * (r * (c * r))) by RELAT_1: 36

        .= (c * (( id X) * r)) by A8, RELAT_1: 36

        .= f by FUNCT_2: 17;

        take h = (cf " );

        thus ( dom h) = ( [#] ( Image f)) by FUNCT_2:def 1;

        

         A19: ( rng ( corestr c)) = ( [#] ( Image c)) by FUNCT_2:def 3;

        

         A20: c is one-to-one by A8, FUNCT_2: 23;

        hence ( rng h) = ( [#] X) by A10, A19, TOPS_2: 49;

        (( corestr c) qua Function " ) is one-to-one by A20;

        hence h is one-to-one by A10, A20, TOPS_2:def 4;

        ( corestr c) is one-to-one by A8, FUNCT_2: 23;

        then (r * ( id the carrier of ( Image c))) = (( id X) * (cf " )) by A10, A19, A18, TOPS_2: 52;

        then (r * ( id ( Image c))) = (cf " ) by FUNCT_2: 17;

        hence h is continuous by A11, A12, TOPS_2: 43;

        ( corestr c) is continuous by WAYBEL18: 10;

        hence thesis by A10, A19, A20, TOPS_2: 51;

      end;

    end

    theorem :: WAYBEL25:8

    for S,T,X,Y be non empty TopSpace st the TopStruct of S = the TopStruct of T & the TopStruct of X = the TopStruct of Y & S is_Retract_of X holds T is_Retract_of Y

    proof

      let S,T,X,Y be non empty TopSpace such that

       A1: the TopStruct of S = the TopStruct of T and

       A2: the TopStruct of X = the TopStruct of Y;

      given c be continuous Function of S, X, r be continuous Function of X, S such that

       A3: (r * c) = ( id S);

      reconsider rr = r as continuous Function of Y, T by A1, A2, YELLOW12: 36;

      reconsider cc = c as continuous Function of T, Y by A1, A2, YELLOW12: 36;

      take cc, rr;

      thus thesis by A1, A3;

    end;

    theorem :: WAYBEL25:9

    for T,S1,S2 be non empty TopStruct st (S1,S2) are_homeomorphic & S1 is_Retract_of T holds S2 is_Retract_of T

    proof

      let T,S1,S2 be non empty TopStruct such that

       A1: (S1,S2) are_homeomorphic and

       A2: S1 is_Retract_of T;

      consider G be Function of S1, S2 such that

       A3: G is being_homeomorphism by A1;

      consider H be Function of T, T such that

       A4: H is continuous and

       A5: (H * H) = H and

       A6: (( Image H),S1) are_homeomorphic by A2;

      take H;

      consider F be Function of ( Image H), S1 such that

       A7: F is being_homeomorphism by A6;

      (G * F) is being_homeomorphism by A3, A7, TOPS_2: 57;

      hence thesis by A4, A5;

    end;

    theorem :: WAYBEL25:10

    for S,T be non empty TopSpace st T is injective & S is_Retract_of T holds S is injective

    proof

      let S,T be non empty TopSpace such that

       A1: T is injective and

       A2: S is_Retract_of T;

      consider h be Function of T, T such that

       A3: h is continuous and

       A4: (h * h) = h and

       A5: (( Image h),S) are_homeomorphic by A2;

      set F = ( corestr h);

      for W be Point of T st W in the carrier of ( Image h) holds (F . W) = W

      proof

        let W be Point of T;

        assume W in the carrier of ( Image h);

        then W in ( rng h) by WAYBEL18: 9;

        then ex x be object st x in ( dom h) & W = (h . x) by FUNCT_1:def 3;

        hence thesis by A4, FUNCT_1: 13;

      end;

      then

       A6: F is being_a_retraction by BORSUK_1:def 16;

      ( corestr h) is continuous by A3, WAYBEL18: 10;

      then ( Image h) is_a_retract_of T by A6, BORSUK_1:def 17;

      then ( Image h) is injective by A1, WAYBEL18: 8;

      hence thesis by A5, Th6;

    end;

    theorem :: WAYBEL25:11

    for J be injective non empty TopSpace, Y be non empty TopSpace st J is SubSpace of Y holds J is_Retract_of Y

    proof

      let J be injective non empty TopSpace, Y be non empty TopSpace;

      assume

       A1: J is SubSpace of Y;

      then

      consider f be Function of Y, J such that

       A2: f is continuous and

       A3: (f | the carrier of J) = ( id J) by WAYBEL18:def 5;

      

       A4: the carrier of J c= the carrier of Y by A1, BORSUK_1: 1;

      then

      reconsider ff = f as Function of Y, Y by FUNCT_2: 7;

      ex ff be Function of Y, Y st ff is continuous & (ff * ff) = ff & (( Image ff),J) are_homeomorphic

      proof

        reconsider M = ( [#] J) as non empty Subset of Y by A1, BORSUK_1: 1;

        take ff;

        thus ff is continuous by A1, A2, PRE_TOPC: 26;

        

         A5: ( dom f) = the carrier of Y by FUNCT_2:def 1;

        

         A6: for x be object st x in the carrier of Y holds ((f * f) . x) = (f . x)

        proof

          let x be object;

          assume

           A7: x in the carrier of Y;

          

          hence ((f * f) . x) = (f . (f . x)) by A5, FUNCT_1: 13

          .= (( id J) . (f . x)) by A3, A7, FUNCT_1: 49, FUNCT_2: 5

          .= (f . x) by A7, FUNCT_1: 18, FUNCT_2: 5;

        end;

        ( dom (ff * ff)) = the carrier of Y by FUNCT_2:def 1;

        hence (ff * ff) = ff by A5, A6, FUNCT_1: 2;

        

         A8: ( rng f) = the carrier of J

        proof

          thus ( rng f) c= the carrier of J;

          let y be object;

          assume

           A9: y in the carrier of J;

          then y in the carrier of Y by A4;

          then

           A10: y in ( dom f) by FUNCT_2:def 1;

          (f . y) = ((f | the carrier of J) . y) by A9, FUNCT_1: 49

          .= y by A3, A9, FUNCT_1: 18;

          hence thesis by A10, FUNCT_1:def 3;

        end;

        the carrier of (Y | M) = ( [#] (Y | M))

        .= the carrier of J by PRE_TOPC:def 5;

        then ( Image ff) = the TopStruct of J by A1, A8, TSEP_1: 5;

        hence thesis by YELLOW14: 19;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL25:12

    

     Th12: for L be complete continuous LATTICE, T be Scott TopAugmentation of L holds T is injective

    proof

      let L be complete continuous LATTICE, T be Scott TopAugmentation of L;

      let X be non empty TopSpace, f be Function of X, T such that

       A1: f is continuous;

      let Y be non empty TopSpace such that

       A2: X is SubSpace of Y;

      deffunc F( set) = ( "\/" ({ ( inf (f .: (V /\ the carrier of X))) where V be open Subset of Y : $1 in V },T));

      consider g be Function of the carrier of Y, the carrier of T such that

       A3: for x be Element of Y holds (g . x) = F(x) from FUNCT_2:sch 4;

      reconsider g as Function of Y, T;

      take g;

      

       A4: ( dom f) = the carrier of X by FUNCT_2:def 1;

      

       A5: for P be Subset of T st P is open holds (g " P) is open

      proof

        let P be Subset of T;

        assume P is open;

        then

        reconsider P as open Subset of T;

        for x be set holds x in (g " P) iff ex Q be Subset of Y st Q is open & Q c= (g " P) & x in Q

        proof

          let x be set;

          thus x in (g " P) implies ex Q be Subset of Y st Q is open & Q c= (g " P) & x in Q

          proof

            assume

             A6: x in (g " P);

            then

            reconsider y = x as Point of Y;

            set A = { ( inf (f .: (V /\ the carrier of X))) where V be open Subset of Y : y in V };

            A c= the carrier of T

            proof

              let a be object;

              assume a in A;

              then ex V be open Subset of Y st a = ( inf (f .: (V /\ the carrier of X))) & y in V;

              hence thesis;

            end;

            then

            reconsider A as Subset of T;

            

             A7: ( inf (f .: (( [#] Y) /\ the carrier of X))) in A;

            

             A8: A is directed

            proof

              let a,b be Element of T;

              assume a in A;

              then

              consider Va be open Subset of Y such that

               A9: a = ( inf (f .: (Va /\ the carrier of X))) and

               A10: y in Va;

              assume b in A;

              then

              consider Vb be open Subset of Y such that

               A11: b = ( inf (f .: (Vb /\ the carrier of X))) and

               A12: y in Vb;

              take ( inf (f .: ((Va /\ Vb) /\ the carrier of X)));

              y in (Va /\ Vb) by A10, A12, XBOOLE_0:def 4;

              hence ( inf (f .: ((Va /\ Vb) /\ the carrier of X))) in A;

              ((Va /\ Vb) /\ the carrier of X) c= (Vb /\ the carrier of X) by XBOOLE_1: 17, XBOOLE_1: 26;

              then

               A13: (f .: ((Va /\ Vb) /\ the carrier of X)) c= (f .: (Vb /\ the carrier of X)) by RELAT_1: 123;

              ((Va /\ Vb) /\ the carrier of X) c= (Va /\ the carrier of X) by XBOOLE_1: 17, XBOOLE_1: 26;

              then (f .: ((Va /\ Vb) /\ the carrier of X)) c= (f .: (Va /\ the carrier of X)) by RELAT_1: 123;

              hence thesis by A9, A11, A13, WAYBEL_7: 1;

            end;

            

             A14: (g . y) = ( sup A) by A3;

            (g . y) in P by A6, FUNCT_2: 38;

            then A meets P by A14, A7, A8, WAYBEL11:def 1;

            then

            consider b be object such that

             A15: b in A and

             A16: b in P by XBOOLE_0: 3;

            consider B be open Subset of Y such that

             A17: b = ( inf (f .: (B /\ the carrier of X))) and

             A18: y in B by A15;

            reconsider b as Element of T by A17;

            take B;

            thus B is open;

            thus B c= (g " P)

            proof

              let a be object;

              assume

               A19: a in B;

              then

              reconsider a as Point of Y;

              

               A20: (g . a) = F(a) by A3;

              b in { ( inf (f .: (V /\ the carrier of X))) where V be open Subset of Y : a in V } by A17, A19;

              then b <= (g . a) by A20, YELLOW_2: 22;

              then (g . a) in P by A16, WAYBEL_0:def 20;

              hence thesis by FUNCT_2: 38;

            end;

            thus thesis by A18;

          end;

          thus thesis;

        end;

        hence thesis by TOPS_1: 25;

      end;

      set gX = (g | the carrier of X);

      

       A21: the carrier of X c= the carrier of Y by A2, BORSUK_1: 1;

      

       A22: for a be object st a in the carrier of X holds (gX . a) = (f . a)

      proof

        let a be object;

        assume a in the carrier of X;

        then

        reconsider x = a as Point of X;

        reconsider y = x as Point of Y by A21;

        set A = { ( inf (f .: (V /\ the carrier of X))) where V be open Subset of Y : y in V };

        A c= the carrier of T

        proof

          let a be object;

          assume a in A;

          then ex V be open Subset of Y st a = ( inf (f .: (V /\ the carrier of X))) & y in V;

          hence thesis;

        end;

        then

        reconsider A as Subset of T;

        

         A23: (f . x) is_>=_than A

        proof

          let z be Element of T;

          assume z in A;

          then

          consider V be open Subset of Y such that

           A24: z = ( inf (f .: (V /\ the carrier of X))) and

           A25: y in V;

          

           A26: ex_inf_of ((f .: (V /\ the carrier of X)),T) by YELLOW_0: 17;

          y in (V /\ the carrier of X) by A25, XBOOLE_0:def 4;

          hence z <= (f . x) by A24, A26, FUNCT_2: 35, YELLOW_4: 2;

        end;

        

         A27: for b be Element of T st b is_>=_than A holds (f . x) <= b

        proof

          let b be Element of T such that

           A28: for k be Element of T st k in A holds k <= b;

          

           A29: for V be open Subset of X st x in V holds ( inf (f .: V)) <= b

          proof

            let V be open Subset of X;

            V in the topology of X by PRE_TOPC:def 2;

            then

            consider Q be Subset of Y such that

             A30: Q in the topology of Y and

             A31: V = (Q /\ ( [#] X)) by A2, PRE_TOPC:def 4;

            reconsider Q as open Subset of Y by A30, PRE_TOPC:def 2;

            assume x in V;

            then y in Q by A31, XBOOLE_0:def 4;

            then ( inf (f .: (Q /\ the carrier of X))) in A;

            hence thesis by A28, A31;

          end;

          

           A32: b is_>=_than ( waybelow (f . x))

          proof

            let w be Element of T;

            

             A33: ( wayabove w) is open by WAYBEL11: 36;

            

             A34: ex_inf_of ((f .: (f " ( wayabove w))),T) by YELLOW_0: 17;

            

             A35: w <= ( inf ( wayabove w)) by WAYBEL14: 9;

             ex_inf_of (( wayabove w),T) by YELLOW_0: 17;

            then ( inf ( wayabove w)) <= ( inf (f .: (f " ( wayabove w)))) by A34, FUNCT_1: 75, YELLOW_0: 35;

            then

             A36: w <= ( inf (f .: (f " ( wayabove w)))) by A35, ORDERS_2: 3;

            assume w in ( waybelow (f . x));

            then w << (f . x) by WAYBEL_3: 7;

            then (f . x) in ( wayabove w) by WAYBEL_3: 8;

            then

             A37: x in (f " ( wayabove w)) by FUNCT_2: 38;

            ( [#] T) <> {} ;

            then (f " ( wayabove w)) is open by A1, A33, TOPS_2: 43;

            then ( inf (f .: (f " ( wayabove w)))) <= b by A29, A37;

            hence w <= b by A36, ORDERS_2: 3;

          end;

          (f . x) = ( sup ( waybelow (f . x))) by WAYBEL_3:def 5;

          hence thesis by A32, YELLOW_0: 32;

        end;

        

        thus (gX . a) = (g . y) by FUNCT_1: 49

        .= F(y) by A3

        .= (f . a) by A23, A27, YELLOW_0: 30;

      end;

      ( [#] T) <> {} ;

      hence g is continuous by A5, TOPS_2: 43;

      ( dom gX) = (( dom g) /\ the carrier of X) by RELAT_1: 61

      .= (the carrier of Y /\ the carrier of X) by FUNCT_2:def 1

      .= the carrier of X by A2, BORSUK_1: 1, XBOOLE_1: 28;

      hence thesis by A4, A22, FUNCT_1: 2;

    end;

    registration

      let L be complete continuous LATTICE;

      cluster Scott -> injective for TopAugmentation of L;

      coherence by Th12;

    end

    registration

      let T be injective non empty TopSpace;

      cluster the TopStruct of T -> injective;

      coherence by WAYBEL18: 16;

    end

    begin

    definition

      let T be TopStruct;

      :: WAYBEL25:def2

      func Omega T -> strict TopRelStr means

      : Def2: the TopStruct of it = the TopStruct of T & for x,y be Element of it holds x <= y iff ex Y be Subset of T st Y = {y} & x in ( Cl Y);

      existence

      proof

        defpred P[ object, object] means ex Y be Subset of T st Y = {$2} & $1 in ( Cl Y);

        consider R be Relation of the carrier of T such that

         A1: for x,y be object holds [x, y] in R iff x in the carrier of T & y in the carrier of T & P[x, y] from RELSET_1:sch 1;

        take G = TopRelStr (# the carrier of T, R, the topology of T #);

        thus the TopStruct of G = the TopStruct of T;

        thus for x,y be Element of G holds x <= y iff ex Y be Subset of T st Y = {y} & x in ( Cl Y) by A1;

      end;

      uniqueness

      proof

        let R1,R2 be strict TopRelStr such that

         A2: the TopStruct of R1 = the TopStruct of T and

         A3: for x,y be Element of R1 holds x <= y iff ex Y be Subset of T st Y = {y} & x in ( Cl Y) and

         A4: the TopStruct of R2 = the TopStruct of T and

         A5: for x,y be Element of R2 holds x <= y iff ex Y be Subset of T st Y = {y} & x in ( Cl Y);

        the InternalRel of R1 = the InternalRel of R2

        proof

          let x,y be object;

          hereby

            assume

             A6: [x, y] in the InternalRel of R1;

            then

            reconsider x1 = x, y1 = y as Element of R1 by ZFMISC_1: 87;

            reconsider x2 = x, y2 = y as Element of R2 by A2, A4, A6, ZFMISC_1: 87;

            x1 <= y1 by A6;

            then ex Y be Subset of T st Y = {y1} & x1 in ( Cl Y) by A3;

            then x2 <= y2 by A5;

            hence [x, y] in the InternalRel of R2;

          end;

          assume

           A7: [x, y] in the InternalRel of R2;

          then

          reconsider x2 = x, y2 = y as Element of R2 by ZFMISC_1: 87;

          reconsider x1 = x, y1 = y as Element of R1 by A2, A4, A7, ZFMISC_1: 87;

          x2 <= y2 by A7;

          then ex Y be Subset of T st Y = {y2} & x2 in ( Cl Y) by A5;

          then x1 <= y1 by A3;

          hence thesis;

        end;

        hence thesis by A2, A4;

      end;

    end

    

     Lm1: for T be TopStruct holds the carrier of T = the carrier of ( Omega T)

    proof

      let T be TopStruct;

       the TopStruct of T = the TopStruct of ( Omega T) by Def2;

      hence thesis;

    end;

    registration

      let T be empty TopStruct;

      cluster ( Omega T) -> empty;

      coherence

      proof

        the carrier of ( Omega T) = the carrier of T by Lm1;

        hence the carrier of ( Omega T) is empty;

      end;

    end

    registration

      let T be non empty TopStruct;

      cluster ( Omega T) -> non empty;

      coherence

      proof

        the carrier of ( Omega T) = the carrier of T by Lm1;

        hence the carrier of ( Omega T) is non empty;

      end;

    end

    registration

      let T be TopSpace;

      cluster ( Omega T) -> TopSpace-like;

      coherence

      proof

        

         A1: the TopStruct of ( Omega T) = the TopStruct of T by Def2;

        hence the carrier of ( Omega T) in the topology of ( Omega T) by PRE_TOPC:def 1;

        thus thesis by A1, PRE_TOPC:def 1;

      end;

    end

    registration

      let T be TopStruct;

      cluster ( Omega T) -> reflexive;

      coherence

      proof

        let x be object;

        assume

         A1: x in the carrier of ( Omega T);

        then

        reconsider T9 = T as non empty TopStruct;

        reconsider a = x as Element of ( Omega T) by A1;

        reconsider t9 = x as Element of T9 by A1, Lm1;

        consider Y be Subset of T such that

         A2: Y = {t9};

        

         A3: Y c= ( Cl Y) by PRE_TOPC: 18;

        a in Y by A2, TARSKI:def 1;

        then a <= a by A2, A3, Def2;

        hence thesis;

      end;

    end

    

     Lm2: for T be TopStruct, x,y be Element of T, X,Y be Subset of T st X = {x} & Y = {y} holds x in ( Cl Y) iff ( Cl X) c= ( Cl Y)

    proof

      let T be TopStruct, x,y be Element of T, X,Y be Subset of T;

      assume that

       A1: X = {x} and

       A2: Y = {y};

      hereby

        assume x in ( Cl Y);

        then for V be Subset of T st V is open holds (x in V implies y in V) by A2, YELLOW14: 21;

        hence ( Cl X) c= ( Cl Y) by A1, A2, YELLOW14: 22;

      end;

      assume ( Cl X) c= ( Cl Y);

      hence thesis by A1, YELLOW14: 20;

    end;

    registration

      let T be TopStruct;

      cluster ( Omega T) -> transitive;

      coherence

      proof

        let x,y,z be object;

        assume that

         A1: x in the carrier of ( Omega T) and

         A2: y in the carrier of ( Omega T) and

         A3: z in the carrier of ( Omega T) and

         A4: [x, y] in the InternalRel of ( Omega T) and

         A5: [y, z] in the InternalRel of ( Omega T);

        reconsider a = x, b = y, c = z as Element of ( Omega T) by A1, A2, A3;

        a <= b by A4;

        then

        consider Y2 be Subset of T such that

         A6: Y2 = {b} and

         A7: a in ( Cl Y2) by Def2;

         the TopStruct of ( Omega T) = the TopStruct of T by Def2;

        then

        reconsider t3 = z as Element of T by A3;

        b <= c by A5;

        then

        consider Y3 be Subset of T such that

         A8: Y3 = {c} and

         A9: b in ( Cl Y3) by Def2;

        Y3 = {t3} by A8;

        then ( Cl Y2) c= ( Cl Y3) by A6, A9, Lm2;

        then a <= c by A7, A8, Def2;

        hence thesis;

      end;

    end

    registration

      let T be T_0-TopSpace;

      cluster ( Omega T) -> antisymmetric;

      coherence

      proof

        let x,y be object;

        assume that

         A1: x in the carrier of ( Omega T) and

         A2: y in the carrier of ( Omega T) and

         A3: [x, y] in the InternalRel of ( Omega T) and

         A4: [y, x] in the InternalRel of ( Omega T);

        reconsider a = x, b = y as Element of ( Omega T) by A1, A2;

        b <= a by A4;

        then

         A5: ex Y1 be Subset of T st Y1 = {a} & b in ( Cl Y1) by Def2;

         the TopStruct of ( Omega T) = the TopStruct of T by Def2;

        then

        reconsider t1 = x, t2 = y as Element of T by A1, A2;

        a <= b by A3;

        then ex Y2 be Subset of T st Y2 = {b} & a in ( Cl Y2) by Def2;

        then for V be Subset of T holds not V is open or (t1 in V implies t2 in V) & (t2 in V implies t1 in V) by A5, YELLOW14: 21;

        hence thesis by T_0TOPSP:def 7;

      end;

    end

    theorem :: WAYBEL25:13

    

     Th13: for S,T be TopSpace st the TopStruct of S = the TopStruct of T holds ( Omega S) = ( Omega T)

    proof

      let S,T be TopSpace such that

       A1: the TopStruct of S = the TopStruct of T;

      

       A2: the TopStruct of ( Omega S) = the TopStruct of S by Def2

      .= the TopStruct of ( Omega T) by A1, Def2;

      the InternalRel of ( Omega S) = the InternalRel of ( Omega T)

      proof

        let a,b be object;

        thus [a, b] in the InternalRel of ( Omega S) implies [a, b] in the InternalRel of ( Omega T)

        proof

          assume

           A3: [a, b] in the InternalRel of ( Omega S);

          then

          reconsider s1 = a, s2 = b as Element of ( Omega S) by ZFMISC_1: 87;

          reconsider t1 = s1, t2 = s2 as Element of ( Omega T) by A2;

          s1 <= s2 by A3;

          then

          consider Y be Subset of S such that

           A4: Y = {s2} and

           A5: s1 in ( Cl Y) by Def2;

          reconsider Z = Y as Subset of T by A1;

          t1 in ( Cl Z) by A1, A5, TOPS_3: 80;

          then t1 <= t2 by A4, Def2;

          hence thesis;

        end;

        assume

         A6: [a, b] in the InternalRel of ( Omega T);

        then

        reconsider s1 = a, s2 = b as Element of ( Omega T) by ZFMISC_1: 87;

        reconsider t1 = s1, t2 = s2 as Element of ( Omega S) by A2;

        s1 <= s2 by A6;

        then

        consider Y be Subset of T such that

         A7: Y = {s2} and

         A8: s1 in ( Cl Y) by Def2;

        reconsider Z = Y as Subset of S by A1;

        t1 in ( Cl Z) by A1, A8, TOPS_3: 80;

        then t1 <= t2 by A7, Def2;

        hence thesis;

      end;

      hence thesis by A2;

    end;

    theorem :: WAYBEL25:14

    for M be non empty set, T be non empty TopSpace holds the RelStr of ( Omega ( product (M --> T))) = the RelStr of ( product (M --> ( Omega T)))

    proof

      let M be non empty set, T be non empty TopSpace;

      

       A1: ( dom ( Carrier (M --> T))) = M by PARTFUN1:def 2

      .= ( dom ( Carrier (M --> ( Omega T)))) by PARTFUN1:def 2;

      

       A2: for i be object st i in ( dom ( Carrier (M --> T))) holds (( Carrier (M --> T)) . i) = (( Carrier (M --> ( Omega T))) . i)

      proof

        let i be object;

        assume i in ( dom ( Carrier (M --> T)));

        then

         A3: i in M;

        then

        consider R1 be 1-sorted such that

         A4: R1 = ((M --> T) . i) and

         A5: (( Carrier (M --> T)) . i) = the carrier of R1 by PRALG_1:def 15;

        consider R2 be 1-sorted such that

         A6: R2 = ((M --> ( Omega T)) . i) and

         A7: (( Carrier (M --> ( Omega T))) . i) = the carrier of R2 by A3, PRALG_1:def 15;

        the carrier of R1 = the carrier of T by A3, A4, FUNCOP_1: 7

        .= the carrier of ( Omega T) by Lm1

        .= the carrier of R2 by A3, A6, FUNCOP_1: 7;

        hence thesis by A5, A7;

      end;

      

       A8: the carrier of ( Omega ( product (M --> T))) = the carrier of ( product (M --> T)) by Lm1

      .= ( product ( Carrier (M --> T))) by WAYBEL18:def 3

      .= ( product ( Carrier (M --> ( Omega T)))) by A1, A2, FUNCT_1: 2;

      

       A9: the carrier of ( Omega ( product (M --> T))) = the carrier of ( product (M --> T)) by Lm1;

      the InternalRel of ( Omega ( product (M --> T))) = the InternalRel of ( product (M --> ( Omega T)))

      proof

        let x,y be object;

        hereby

          assume

           A10: [x, y] in the InternalRel of ( Omega ( product (M --> T)));

          then

           A11: y in the carrier of ( Omega ( product (M --> T))) by ZFMISC_1: 87;

          

           A12: x in the carrier of ( Omega ( product (M --> T))) by A10, ZFMISC_1: 87;

          then

          reconsider xp = x, yp = y as Element of ( product (M --> ( Omega T))) by A8, A11, YELLOW_1:def 4;

          reconsider p1 = x, p2 = y as Element of ( product (M --> T)) by A12, A11, Lm1;

          reconsider xo = x, yo = y as Element of ( Omega ( product (M --> T))) by A10, ZFMISC_1: 87;

          

           A13: xp in ( product ( Carrier (M --> ( Omega T)))) by A8, A10, ZFMISC_1: 87;

          then

          consider f be Function such that

           A14: xp = f and ( dom f) = ( dom ( Carrier (M --> ( Omega T)))) and for i be object st i in ( dom ( Carrier (M --> ( Omega T)))) holds (f . i) in (( Carrier (M --> ( Omega T))) . i) by CARD_3:def 5;

          yp in ( product ( Carrier (M --> ( Omega T)))) by A8, A10, ZFMISC_1: 87;

          then

          consider g be Function such that

           A15: yp = g and ( dom g) = ( dom ( Carrier (M --> ( Omega T)))) and for i be object st i in ( dom ( Carrier (M --> ( Omega T)))) holds (g . i) in (( Carrier (M --> ( Omega T))) . i) by CARD_3:def 5;

          xo <= yo by A10;

          then

           A16: ex Yp be Subset of ( product (M --> T)) st Yp = {p2} & p1 in ( Cl Yp) by Def2;

          for i be object st i in M holds ex R be RelStr, xi,yi be Element of R st R = ((M --> ( Omega T)) . i) & xi = (f . i) & yi = (g . i) & xi <= yi

          proof

            let i be object;

            assume

             A17: i in M;

            then

            reconsider j = i as Element of M;

            set t1 = (p1 . j), t2 = (p2 . j);

            reconsider xi = t1, yi = t2 as Element of ( Omega T) by Lm1;

            take ( Omega T), xi, yi;

            thus ( Omega T) = ((M --> ( Omega T)) . i) by A17, FUNCOP_1: 7;

            thus xi = (f . i) by A14;

            thus yi = (g . i) by A15;

            (p1 . j) in ( Cl {(p2 . j)}) by A16, YELLOW14: 30;

            hence xi <= yi by Def2;

          end;

          then xp <= yp by A13, A14, A15, YELLOW_1:def 4;

          hence [x, y] in the InternalRel of ( product (M --> ( Omega T)));

        end;

        assume

         A18: [x, y] in the InternalRel of ( product (M --> ( Omega T)));

        then

        reconsider xp = x, yp = y as Element of ( product (M --> ( Omega T))) by ZFMISC_1: 87;

        

         A19: xp <= yp by A18;

        

         A20: x in the carrier of ( product (M --> ( Omega T))) by A18, ZFMISC_1: 87;

        then xp in ( product ( Carrier (M --> ( Omega T)))) by YELLOW_1:def 4;

        then

        consider f,g be Function such that

         A21: f = xp and

         A22: g = yp and

         A23: for i be object st i in M holds ex R be RelStr, xi,yi be Element of R st R = ((M --> ( Omega T)) . i) & xi = (f . i) & yi = (g . i) & xi <= yi by A19, YELLOW_1:def 4;

        

         A24: y in the carrier of ( product (M --> ( Omega T))) by A18, ZFMISC_1: 87;

        then

        reconsider xo = x, yo = y as Element of ( Omega ( product (M --> T))) by A8, A20, YELLOW_1:def 4;

        reconsider p1 = x, p2 = y as Element of ( product (M --> T)) by A8, A9, A20, A24, YELLOW_1:def 4;

        for i be Element of M holds (p1 . i) in ( Cl {(p2 . i)})

        proof

          let i be Element of M;

          consider R1 be RelStr, xi,yi be Element of R1 such that

           A25: R1 = ((M --> ( Omega T)) . i) and

           A26: xi = (f . i) and

           A27: yi = (g . i) and

           A28: xi <= yi by A23;

          reconsider xi, yi as Element of ( Omega T) by A25;

          xi <= yi by A25, A28;

          then ex Y be Subset of T st Y = {yi} & xi in ( Cl Y) by Def2;

          hence thesis by A21, A22, A26, A27;

        end;

        then p1 in ( Cl {p2}) by YELLOW14: 30;

        then xo <= yo by Def2;

        hence thesis;

      end;

      hence thesis by A8, YELLOW_1:def 4;

    end;

    theorem :: WAYBEL25:15

    

     Th15: for S be Scott complete TopLattice holds ( Omega S) = the TopRelStr of S

    proof

      let S be Scott complete TopLattice;

      

       A1: the TopStruct of ( Omega S) = the TopStruct of S by Def2;

      the InternalRel of ( Omega S) = the InternalRel of S

      proof

        let x,y be object;

        hereby

          assume

           A2: [x, y] in the InternalRel of ( Omega S);

          then

           A3: y in the carrier of ( Omega S) by ZFMISC_1: 87;

          x in the carrier of ( Omega S) by A2, ZFMISC_1: 87;

          then

          reconsider t1 = x, t2 = y as Element of S by A3, Lm1;

          reconsider o1 = x, o2 = y as Element of ( Omega S) by A2, ZFMISC_1: 87;

          o1 <= o2 by A2;

          then ex Y2 be Subset of S st Y2 = {o2} & o1 in ( Cl Y2) by Def2;

          then t1 in ( downarrow t2) by WAYBEL11: 9;

          then ex t3 be Element of S st t3 >= t1 & t3 in {t2} by WAYBEL_0:def 15;

          then t1 <= t2 by TARSKI:def 1;

          hence [x, y] in the InternalRel of S;

        end;

        assume

         A4: [x, y] in the InternalRel of S;

        then

        reconsider t1 = x, t2 = y as Element of S by ZFMISC_1: 87;

        reconsider o1 = x, o2 = y as Element of ( Omega S) by A1, A4, ZFMISC_1: 87;

        

         A5: t2 in {t2} by TARSKI:def 1;

        t1 <= t2 by A4;

        then t1 in ( downarrow t2) by A5, WAYBEL_0:def 15;

        then t1 in ( Cl {t2}) by WAYBEL11: 9;

        then o1 <= o2 by Def2;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    theorem :: WAYBEL25:16

    

     Th16: for L be complete LATTICE, S be Scott TopAugmentation of L holds the RelStr of ( Omega S) = the RelStr of L

    proof

      let L be complete LATTICE, S be Scott TopAugmentation of L;

       the TopRelStr of S = ( Omega S) by Th15;

      hence thesis by YELLOW_9:def 4;

    end;

    registration

      let S be Scott complete TopLattice;

      cluster ( Omega S) -> complete;

      coherence

      proof

        set T = the Scott TopAugmentation of S;

        

         A1: the RelStr of ( Omega T) = the RelStr of S by Th16;

        the topology of S = ( sigma S) by WAYBEL14: 23

        .= the topology of T by YELLOW_9: 51;

        then the TopStruct of S = the TopStruct of T by A1, Lm1;

        then ( Omega S) = ( Omega T) by Th13;

        hence thesis by A1, YELLOW_0: 3;

      end;

    end

    theorem :: WAYBEL25:17

    

     Th17: for T be non empty TopSpace, S be non empty SubSpace of T holds ( Omega S) is full SubRelStr of ( Omega T)

    proof

      let T be non empty TopSpace, S be non empty SubSpace of T;

      

       A1: the carrier of S c= the carrier of T by BORSUK_1: 1;

      

       A2: the carrier of ( Omega S) = the carrier of S by Lm1;

      

       A3: the InternalRel of ( Omega S) c= the InternalRel of ( Omega T)

      proof

        let x,y be object;

        assume

         A4: [x, y] in the InternalRel of ( Omega S);

        then

        reconsider o1 = x, o2 = y as Element of ( Omega S) by ZFMISC_1: 87;

        

         A5: y in the carrier of ( Omega S) by A4, ZFMISC_1: 87;

        then

        reconsider s2 = y as Element of S by Lm1;

        x in the carrier of ( Omega S) by A4, ZFMISC_1: 87;

        then

        reconsider o3 = x, o4 = y as Element of ( Omega T) by A1, A2, A5, Lm1;

        reconsider t2 = y as Element of T by A1, A2, A5;

        ( Cl {s2}) = (( Cl {t2}) /\ ( [#] S)) by PRE_TOPC: 17;

        then

         A6: ( Cl {s2}) c= ( Cl {t2}) by XBOOLE_1: 17;

        o1 <= o2 by A4;

        then ex Y2 be Subset of S st Y2 = {o2} & o1 in ( Cl Y2) by Def2;

        then o3 <= o4 by A6, Def2;

        hence thesis;

      end;

      

       A7: the InternalRel of ( Omega S) = (the InternalRel of ( Omega T) |_2 the carrier of ( Omega S))

      proof

        let x,y be object;

        thus [x, y] in the InternalRel of ( Omega S) implies [x, y] in (the InternalRel of ( Omega T) |_2 the carrier of ( Omega S)) by A3, XBOOLE_0:def 4;

        assume

         A8: [x, y] in (the InternalRel of ( Omega T) |_2 the carrier of ( Omega S));

        then

         A9: y in the carrier of ( Omega S) by ZFMISC_1: 87;

        

         A10: x in the carrier of ( Omega S) by A8, ZFMISC_1: 87;

        then

        reconsider t1 = x, t2 = y as Element of T by A1, A2, A9;

        reconsider o1 = x, o2 = y as Element of ( Omega T) by A1, A2, A10, A9, Lm1;

         [x, y] in the InternalRel of ( Omega T) by A8, XBOOLE_0:def 4;

        then o1 <= o2;

        then

         A11: ex Y be Subset of T st Y = {t2} & t1 in ( Cl Y) by Def2;

        reconsider s1 = x, s2 = y as Element of S by A10, A9, Lm1;

        reconsider o3 = x, o4 = y as Element of ( Omega S) by A8, ZFMISC_1: 87;

        ( Cl {s2}) = (( Cl {t2}) /\ ( [#] S)) by PRE_TOPC: 17;

        then s1 in ( Cl {s2}) by A11, XBOOLE_0:def 4;

        then o3 <= o4 by Def2;

        hence thesis;

      end;

      the carrier of ( Omega S) c= the carrier of ( Omega T) by A1, A2, Lm1;

      hence thesis by A3, A7, YELLOW_0:def 13, YELLOW_0:def 14;

    end;

    theorem :: WAYBEL25:18

    

     Th18: for S,T be TopSpace, h be Function of S, T, g be Function of ( Omega S), ( Omega T) st h = g & h is being_homeomorphism holds g is isomorphic

    proof

      let S,T be TopSpace, h be Function of S, T, g be Function of ( Omega S), ( Omega T);

      assume that

       A1: h = g and

       A2: h is being_homeomorphism;

      

       A3: ( dom h) = ( [#] S) by A2;

      

       A4: ( rng h) = ( [#] T) by A2;

      

       A5: the carrier of T = the carrier of ( Omega T) by Lm1;

      

       A6: the carrier of S = the carrier of ( Omega S) by Lm1;

      

       A7: h is one-to-one by A2;

      per cases ;

        suppose

         A8: S is non empty & T is non empty;

        then

        reconsider s = S, t = T as non empty TopSpace;

        reconsider f = g as Function of ( Omega s), ( Omega t);

        for x,y be Element of ( Omega s) holds x <= y iff (f . x) <= (f . y)

        proof

          let x,y be Element of ( Omega s);

          

           A9: ( dom f) = ( [#] S) by A1, A2

          .= the carrier of S;

          reconsider Z = {((f " ) . (f . y))} as Subset of s by Lm1;

          

           A10: (h " ) is being_homeomorphism by A2, A8, TOPS_2: 56;

          

           A11: f is onto by A1, A4, A5, FUNCT_2:def 3;

          then

           A12: (f " ) = (f qua Function " ) by A1, A7, TOPS_2:def 4;

          

           A13: ( dom h) = the carrier of ( Omega s) by A3, Lm1;

          

          then

           A14: y = ((h qua Function " ) . (h . y)) by A7, FUNCT_1: 34

          .= ((f " ) . (f . y)) by A11, A1, A7, TOPS_2:def 4;

          hereby

            reconsider Z = {(f . y)} as Subset of t by Lm1;

            assume x <= y;

            then

            consider Y be Subset of s such that

             A15: Y = {y} and

             A16: x in ( Cl Y) by Def2;

            

             A17: ( Im (h,y)) = Z by A1, A13, FUNCT_1: 59;

            (f . x) in (f .: ( Cl Y)) by A16, FUNCT_2: 35;

            then (h . x) in ( Cl (h .: Y)) by A1, A2, TOPS_2: 60;

            hence (f . x) <= (f . y) by A1, A15, A17, Def2;

          end;

          assume (f . x) <= (f . y);

          then

          consider Y be Subset of t such that

           A18: Y = {(f . y)} and

           A19: (f . x) in ( Cl Y) by Def2;

          

           A20: (f " ) = (h " ) by A1, A5, A6;

          

           A21: x = ((f " ) . (f . x)) by A1, A7, A12, A13, FUNCT_1: 34;

          ((f " ) . (f . x)) in ((f " ) .: ( Cl Y)) by A19, FUNCT_2: 35;

          then

           A22: ((h " ) . (h . x)) in ( Cl ((h " ) .: Y)) by A1, A10, A20, TOPS_2: 60;

          ((f " ) .: Y) = (f " Y) by A1, A7, A12, FUNCT_1: 85

          .= Z by A1, A6, A7, A18, A14, A9, FINSEQ_5: 4;

          hence thesis by A1, A20, A22, A21, A14, Def2;

        end;

        hence thesis by A1, A5, A7, A4, WAYBEL_0: 66;

      end;

        suppose S is empty or T is empty;

        then

        reconsider s = S, t = T as empty TopSpace by A3, A4;

        

         A23: ( Omega t) is empty;

        ( Omega s) is empty;

        hence thesis by A23, WAYBEL_0:def 38;

      end;

    end;

    theorem :: WAYBEL25:19

    

     Th19: for S,T be TopSpace st (S,T) are_homeomorphic holds (( Omega S),( Omega T)) are_isomorphic

    proof

      let S,T be TopSpace;

      assume (S,T) are_homeomorphic ;

      then

      consider h be Function of S, T such that

       A1: h is being_homeomorphism;

      

       A2: the carrier of T = the carrier of ( Omega T) by Lm1;

      the carrier of S = the carrier of ( Omega S) by Lm1;

      then

      reconsider f = h as Function of ( Omega S), ( Omega T) by A2;

      take f;

      thus thesis by A1, Th18;

    end;

    

     Lm3: for S,T be non empty RelStr, f be Function of S, S, g be Function of T, T st the RelStr of S = the RelStr of T & f = g & f is projection holds g is projection by WAYBEL_9: 1;

    theorem :: WAYBEL25:20

    

     Th20: for T be injective T_0-TopSpace holds ( Omega T) is complete continuous LATTICE

    proof

      let T be injective T_0-TopSpace;

      set S = Sierpinski_Space , B = ( BoolePoset { 0 });

      consider M be non empty set such that

       A1: T is_Retract_of ( product (M --> S)) by WAYBEL18: 19;

      consider f be Function of ( product (M --> S)), ( product (M --> S)) such that

       A2: f is continuous and

       A3: (f * f) = f and

       A4: (( Image f),T) are_homeomorphic by A1;

      

       A5: ( the RelStr of ( Omega ( Image f)),( Omega ( Image f))) are_isomorphic by WAYBEL13: 26;

      (( Omega ( Image f)),( Omega T)) are_isomorphic by A4, Th19;

      then

       A6: ( the RelStr of ( Omega ( Image f)),( Omega T)) are_isomorphic by A5, WAYBEL_1: 7;

      ( Omega ( Image f)) is full SubRelStr of ( Omega ( product (M --> S))) by Th17;

      then

       A7: the InternalRel of ( Omega ( Image f)) = (the InternalRel of ( Omega ( product (M --> S))) |_2 the carrier of ( Omega ( Image f))) by YELLOW_0:def 14;

      set TL = the Scott TopAugmentation of ( product (M --> B));

      

       A8: the RelStr of TL = the RelStr of ( product (M --> B)) by YELLOW_9:def 4;

      

       A9: the carrier of TL = the carrier of ( product (M --> S)) by Th3;

      then

      reconsider ff = f as Function of TL, TL;

      

       A10: the topology of TL = the topology of ( product (M --> S)) by WAYBEL18: 15;

      then

       A11: ff is continuous by A2, A9, YELLOW12: 36;

      then ff is idempotent monotone by A3, QUANTAL1:def 9;

      then ff is projection;

      then

      reconsider g = ff as projection Function of ( product (M --> B)), ( product (M --> B)) by A8, Lm3;

      

       A12: the InternalRel of ( Image g) = (the InternalRel of ( product (M --> B)) |_2 the carrier of ( Image g)) by YELLOW_0:def 14;

       the TopStruct of the TopStruct of TL = the TopStruct of TL implies ( Omega the TopStruct of TL) = ( Omega TL) by Th13;

      then

       A13: the RelStr of ( Omega the TopStruct of ( product (M --> S))) = the RelStr of ( product (M --> B)) by A10, A9, Th16;

      g is directed-sups-preserving by A8, A11, WAYBEL21: 6;

      then

       A14: ( Image g) is complete continuous LATTICE by WAYBEL15: 15, YELLOW_2: 35;

      the carrier of ( Image g) = ( rng g) by YELLOW_0:def 15

      .= the carrier of ( Image f) by WAYBEL18: 9

      .= the carrier of ( Omega ( Image f)) by Lm1;

      hence thesis by A13, A14, A6, A12, A7, WAYBEL15: 9, WAYBEL20: 18, YELLOW14: 11, YELLOW14: 12;

    end;

    registration

      let T be injective T_0-TopSpace;

      cluster ( Omega T) -> complete continuous;

      coherence by Th20;

    end

    theorem :: WAYBEL25:21

    

     Th21: for X,Y be non empty TopSpace, f be continuous Function of ( Omega X), ( Omega Y) holds f is monotone

    proof

      let X,Y be non empty TopSpace, f be continuous Function of ( Omega X), ( Omega Y);

      let x,y be Element of ( Omega X);

      reconsider Z = {(f . y)} as Subset of Y by Lm1;

      assume x <= y;

      then

      consider A be Subset of X such that

       A1: A = {y} and

       A2: x in ( Cl A) by Def2;

      

       A3: for G be Subset of Y st G is open holds (f . x) in G implies Z meets G

      proof

        the carrier of X = the carrier of ( Omega X) by Lm1;

        then

        reconsider g = f as Function of X, Y by Lm1;

        let G be Subset of Y such that

         A4: G is open and

         A5: (f . x) in G;

        

         A6: x in (g " G) by A5, FUNCT_2: 38;

        

         A7: the TopStruct of Y = the TopStruct of ( Omega Y) by Def2;

        

         A8: (f . y) in Z by TARSKI:def 1;

         the TopStruct of X = the TopStruct of ( Omega X) by Def2;

        then

         A9: g is continuous by A7, YELLOW12: 36;

        ( [#] Y) <> {} ;

        then (g " G) is open by A4, A9, TOPS_2: 43;

        then A meets (g " G) by A2, A6, PRE_TOPC:def 7;

        then

        consider m be object such that

         A10: m in (A /\ (g " G)) by XBOOLE_0: 4;

        m in A by A10, XBOOLE_0:def 4;

        then

         A11: m = y by A1, TARSKI:def 1;

        m in (g " G) by A10, XBOOLE_0:def 4;

        then (f . y) in G by A11, FUNCT_2: 38;

        then (Z /\ G) <> ( {} Y) by A8, XBOOLE_0:def 4;

        hence thesis;

      end;

      the carrier of Y = the carrier of ( Omega Y) by Lm1;

      then (f . x) in ( Cl Z) by A3, PRE_TOPC:def 7;

      hence (f . x) <= (f . y) by Def2;

    end;

    registration

      let X,Y be non empty TopSpace;

      cluster continuous -> monotone for Function of ( Omega X), ( Omega Y);

      coherence by Th21;

    end

    theorem :: WAYBEL25:22

    

     Th22: for T be non empty TopSpace, x be Element of ( Omega T) holds ( Cl {x}) = ( downarrow x)

    proof

      let T be non empty TopSpace, x be Element of ( Omega T);

      

       A1: the TopStruct of T = the TopStruct of ( Omega T) by Def2;

      hereby

        reconsider Z = {x} as Subset of T by A1;

        let a be object;

        assume

         A2: a in ( Cl {x});

        then

        reconsider b = a as Element of ( Omega T);

        a in ( Cl Z) by A1, A2, TOPS_3: 80;

        then b <= x by Def2;

        hence a in ( downarrow x) by WAYBEL_0: 17;

      end;

      let a be object;

      assume

       A3: a in ( downarrow x);

      then

      reconsider b = a as Element of ( Omega T);

      b <= x by A3, WAYBEL_0: 17;

      then ex Z be Subset of T st Z = {x} & b in ( Cl Z) by Def2;

      hence thesis by A1, TOPS_3: 80;

    end;

    registration

      let T be non empty TopSpace, x be Element of ( Omega T);

      cluster ( Cl {x}) -> non empty lower directed;

      coherence

      proof

        reconsider y = x as Element of ( Omega T);

        ( Cl {y}) = ( downarrow y) by Th22;

        hence thesis;

      end;

      cluster ( downarrow x) -> closed;

      coherence

      proof

        ( Cl {x}) = ( downarrow x) by Th22;

        hence thesis;

      end;

    end

    theorem :: WAYBEL25:23

    

     Th23: for X be TopSpace, A be open Subset of ( Omega X) holds A is upper

    proof

      let X be TopSpace, A be open Subset of ( Omega X);

      let x,y be Element of ( Omega X) such that

       A1: x in A;

      assume x <= y;

      then

       A2: ex Z be Subset of X st Z = {y} & x in ( Cl Z) by Def2;

      then

      reconsider X as non empty TopSpace;

      reconsider y as Element of ( Omega X);

       the TopStruct of X = the TopStruct of ( Omega X) by Def2;

      then x in ( Cl {y}) by A2, TOPS_3: 80;

      then A meets {y} by A1, PRE_TOPC:def 7;

      hence thesis by ZFMISC_1: 50;

    end;

    registration

      let T be TopSpace;

      cluster open -> upper for Subset of ( Omega T);

      coherence by Th23;

    end

     Lm4:

    now

      let X,Y be non empty TopSpace, N be net of ( ContMaps (X,( Omega Y)));

      

       A1: the carrier of Y = the carrier of ( Omega Y) by Lm1;

      the carrier of ( ContMaps (X,( Omega Y))) c= ( Funcs (the carrier of X,the carrier of Y))

      proof

        let f be object;

        assume f in the carrier of ( ContMaps (X,( Omega Y)));

        then ex x be Function of X, ( Omega Y) st x = f & x is continuous by WAYBEL24:def 3;

        hence thesis by A1, FUNCT_2: 8;

      end;

      then

       A2: ( Funcs (the carrier of N,the carrier of ( ContMaps (X,( Omega Y))))) c= ( Funcs (the carrier of N,( Funcs (the carrier of X,the carrier of Y)))) by FUNCT_5: 56;

      the mapping of N in ( Funcs (the carrier of N,the carrier of ( ContMaps (X,( Omega Y))))) by FUNCT_2: 8;

      hence the mapping of N in ( Funcs (the carrier of N,( Funcs (the carrier of X,the carrier of Y)))) by A2;

    end;

    definition

      let I be non empty set, S,T be non empty RelStr, N be net of T, i be Element of I;

      :: WAYBEL25:def3

      func commute (N,i,S) -> strict net of S means

      : Def3: the RelStr of it = the RelStr of N & the mapping of it = (( commute the mapping of N) . i);

      existence

      proof

        the carrier of T c= ( Funcs (I,the carrier of S)) by A1, YELLOW_1: 28;

        then

         A2: ( Funcs (the carrier of N,the carrier of T)) c= ( Funcs (the carrier of N,( Funcs (I,the carrier of S)))) by FUNCT_5: 56;

        

         A3: the mapping of N in ( Funcs (the carrier of N,the carrier of T)) by FUNCT_2: 8;

        then

         A4: ( rng (( commute the mapping of N) . i)) c= the carrier of S by A2, EQUATION: 3;

        ( dom (( commute the mapping of N) . i)) = the carrier of N by A3, A2, EQUATION: 3;

        then

        reconsider f = (( commute the mapping of N) . i) as Function of the carrier of N, the carrier of S by A4, FUNCT_2:def 1, RELSET_1: 4;

        set A = NetStr (# the carrier of N, the InternalRel of N, f #);

        

         A5: the RelStr of A = the RelStr of N;

        ( [#] N) is directed by WAYBEL_0:def 6;

        then ( [#] A) is directed by A5, WAYBEL_0: 3;

        then

        reconsider A as strict net of S by A5, WAYBEL_0:def 6, WAYBEL_8: 13;

        take A;

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: WAYBEL25:24

    

     Th24: for X,Y be non empty TopSpace, N be net of ( ContMaps (X,( Omega Y))), i be Element of N, x be Point of X holds (the mapping of ( commute (N,x,( Omega Y))) . i) = ((the mapping of N . i) . x)

    proof

      let X,Y be non empty TopSpace, N be net of ( ContMaps (X,( Omega Y))), i be Element of N, x be Point of X;

      

       A1: the mapping of N in ( Funcs (the carrier of N,( Funcs (the carrier of X,the carrier of Y)))) by Lm4;

      ( ContMaps (X,( Omega Y))) is SubRelStr of (( Omega Y) |^ the carrier of X) by WAYBEL24:def 3;

      then the carrier of ( ContMaps (X,( Omega Y))) c= the carrier of (( Omega Y) |^ the carrier of X) by YELLOW_0:def 13;

      

      hence (the mapping of ( commute (N,x,( Omega Y))) . i) = ((( commute the mapping of N) . x) . i) by Def3

      .= ((the mapping of N . i) . x) by A1, FUNCT_6: 56;

    end;

    theorem :: WAYBEL25:25

    

     Th25: for X,Y be non empty TopSpace, N be eventually-directed net of ( ContMaps (X,( Omega Y))), x be Point of X holds ( commute (N,x,( Omega Y))) is eventually-directed

    proof

      let X,Y be non empty TopSpace, N be eventually-directed net of ( ContMaps (X,( Omega Y))), x be Point of X;

      set M = ( commute (N,x,( Omega Y))), L = (( Omega Y) |^ the carrier of X);

      for i be Element of M holds ex j be Element of M st for k be Element of M st j <= k holds (M . i) <= (M . k)

      proof

        let i be Element of M;

        

         A1: ( ContMaps (X,( Omega Y))) is SubRelStr of L by WAYBEL24:def 3;

        then the carrier of ( ContMaps (X,( Omega Y))) c= the carrier of (( Omega Y) |^ the carrier of X) by YELLOW_0:def 13;

        then

         A2: the RelStr of N = the RelStr of M by Def3;

        then

        reconsider a = i as Element of N;

        consider b be Element of N such that

         A3: for c be Element of N st b <= c holds (N . a) <= (N . c) by WAYBEL_0: 11;

        reconsider j = b as Element of M by A2;

        take j;

        let k be Element of M;

        reconsider c = k as Element of N by A2;

        reconsider Na = (N . a), Nc = (N . c) as Element of L by A1, YELLOW_0: 58;

        reconsider A = Na, C = Nc as Element of ( product (the carrier of X --> ( Omega Y))) by YELLOW_1:def 5;

        assume j <= k;

        then b <= c by A2;

        then (N . a) <= (N . c) by A3;

        then Na <= Nc by A1, YELLOW_0: 59;

        then A <= C by YELLOW_1:def 5;

        then

         A4: (A . x) <= (C . x) by WAYBEL_3: 28;

        

         A5: (the mapping of M . c) = ((the mapping of N . k) . x) by Th24;

        (the mapping of M . a) = ((the mapping of N . i) . x) by Th24;

        hence thesis by A4, A5;

      end;

      hence thesis by WAYBEL_0: 11;

    end;

    registration

      let X,Y be non empty TopSpace, N be eventually-directed net of ( ContMaps (X,( Omega Y))), x be Point of X;

      cluster ( commute (N,x,( Omega Y))) -> eventually-directed;

      coherence by Th25;

    end

    registration

      let X,Y be non empty TopSpace;

      cluster -> Function-yielding for net of ( ContMaps (X,( Omega Y)));

      coherence ;

    end

     Lm5:

    now

      let X,Y be non empty TopSpace, N be net of ( ContMaps (X,( Omega Y))), i be Element of N;

      thus (the mapping of N . i) is Function of X, ( Omega Y) by WAYBEL24: 21;

      the carrier of Y = the carrier of ( Omega Y) by Lm1;

      hence (the mapping of N . i) is Function of X, Y by WAYBEL24: 21;

    end;

     Lm6:

    now

      let X,Y be non empty TopSpace, N be net of ( ContMaps (X,( Omega Y))), x be Point of X;

      ( ContMaps (X,( Omega Y))) is SubRelStr of (( Omega Y) |^ the carrier of X) by WAYBEL24:def 3;

      then the carrier of ( ContMaps (X,( Omega Y))) c= the carrier of (( Omega Y) |^ the carrier of X) by YELLOW_0:def 13;

      then

       A1: the RelStr of N = the RelStr of ( commute (N,x,( Omega Y))) by Def3;

      

      thus ( dom the mapping of N) = the carrier of N by FUNCT_2:def 1

      .= ( dom the mapping of ( commute (N,x,( Omega Y)))) by A1, FUNCT_2:def 1;

    end;

    theorem :: WAYBEL25:26

    

     Th26: for X be non empty TopSpace, Y be T_0-TopSpace, N be net of ( ContMaps (X,( Omega Y))) st for x be Point of X holds ex_sup_of ( commute (N,x,( Omega Y))) holds ex_sup_of (( rng the mapping of N),(( Omega Y) |^ the carrier of X))

    proof

      let X be non empty TopSpace, Y be T_0-TopSpace, N be net of ( ContMaps (X,( Omega Y))) such that

       A1: for x be Point of X holds ex_sup_of ( commute (N,x,( Omega Y)));

      deffunc F( Element of X) = ( sup ( commute (N,$1,( Omega Y))));

      set n = the mapping of N, L = (( Omega Y) |^ the carrier of X);

      consider f be Function of the carrier of X, the carrier of ( Omega Y) such that

       A2: for u be Element of X holds (f . u) = F(u) from FUNCT_2:sch 4;

      reconsider a = f as Element of L by WAYBEL24: 19;

      ex a be Element of L st ( rng n) is_<=_than a & for b be Element of L st ( rng n) is_<=_than b holds a <= b

      proof

        take a;

        

         A3: ( dom n) = the carrier of N by FUNCT_2:def 1;

        

         A4: L = ( product (the carrier of X --> ( Omega Y))) by YELLOW_1:def 5;

        thus ( rng n) is_<=_than a

        proof

          let k be Element of L;

          reconsider k9 = k, a9 = a as Element of ( product (the carrier of X --> ( Omega Y))) by YELLOW_1:def 5;

          assume k in ( rng n);

          then

          consider i be object such that

           A5: i in ( dom n) and

           A6: k = (n . i) by FUNCT_1:def 3;

          reconsider i as Point of N by A5;

          for u be Element of X holds (k9 . u) <= (a9 . u)

          proof

            let u be Element of X;

             ex_sup_of ( commute (N,u,( Omega Y))) by A1;

            then

             A8: ex_sup_of (( rng the mapping of ( commute (N,u,( Omega Y)))),( Omega Y));

            

             A9: (k9 . u) = (the mapping of ( commute (N,u,( Omega Y))) . i) by A6, Th24;

            ( dom the mapping of ( commute (N,u,( Omega Y)))) = the carrier of N by A3, Lm6;

            then

             A10: (k9 . u) in ( rng the mapping of ( commute (N,u,( Omega Y)))) by A9, FUNCT_1:def 3;

            (a9 . u) = ( sup ( commute (N,u,( Omega Y)))) by A2

            .= ( Sup the mapping of ( commute (N,u,( Omega Y)))) by WAYBEL_2:def 1

            .= ( sup ( rng the mapping of ( commute (N,u,( Omega Y)))));

            hence thesis by A8, A10, YELLOW_4: 1;

          end;

          hence k <= a by A4, WAYBEL_3: 28;

        end;

        let b be Element of L such that

         A11: for k be Element of L st k in ( rng n) holds k <= b;

        reconsider a9 = a, b9 = b as Element of ( product (the carrier of X --> ( Omega Y))) by YELLOW_1:def 5;

        for u be Element of X holds (a9 . u) <= (b9 . u)

        proof

          let u be Element of X;

           ex_sup_of ( commute (N,u,( Omega Y))) by A1;

          then

           A12: ex_sup_of (( rng the mapping of ( commute (N,u,( Omega Y)))),( Omega Y));

          

           A13: ( Omega Y) = ((the carrier of X --> ( Omega Y)) . u);

          

           A14: ( rng the mapping of ( commute (N,u,( Omega Y)))) is_<=_than (b . u)

          proof

            let s be Element of ( Omega Y);

            assume s in ( rng the mapping of ( commute (N,u,( Omega Y))));

            then

            consider i be object such that

             A15: i in ( dom the mapping of ( commute (N,u,( Omega Y)))) and

             A16: (the mapping of ( commute (N,u,( Omega Y))) . i) = s by FUNCT_1:def 3;

            reconsider i as Point of N by A3, A15, Lm6;

            (n . i) is Function of X, ( Omega Y) by WAYBEL24: 21;

            then

            reconsider k = (n . i) as Element of L by WAYBEL24: 19;

            reconsider k9 = k as Element of ( product (the carrier of X --> ( Omega Y))) by YELLOW_1:def 5;

            (n . i) in ( rng n) by A3, FUNCT_1:def 3;

            then k <= b by A11;

            then

             A17: k9 <= b9 by YELLOW_1:def 5;

            s = ((n . i) . u) by A16, Th24;

            hence s <= (b . u) by A13, A17, WAYBEL_3: 28;

          end;

          (a9 . u) = ( sup ( commute (N,u,( Omega Y)))) by A2

          .= ( Sup the mapping of ( commute (N,u,( Omega Y)))) by WAYBEL_2:def 1

          .= ( sup ( rng the mapping of ( commute (N,u,( Omega Y)))));

          hence thesis by A12, A14, YELLOW_0: 30;

        end;

        hence thesis by A4, WAYBEL_3: 28;

      end;

      hence thesis by YELLOW_0: 15;

    end;

    begin

    definition

      let T be non empty TopSpace;

      :: WAYBEL25:def4

      attr T is monotone-convergence means

      : Def4: for D be non empty directed Subset of ( Omega T) holds ex_sup_of (D,( Omega T)) & for V be open Subset of T st ( sup D) in V holds D meets V;

    end

    theorem :: WAYBEL25:27

    

     Th27: for S,T be non empty TopSpace st the TopStruct of S = the TopStruct of T & S is monotone-convergence holds T is monotone-convergence

    proof

      let S,T be non empty TopSpace such that

       A1: the TopStruct of S = the TopStruct of T and

       A2: for D be non empty directed Subset of ( Omega S) holds ex_sup_of (D,( Omega S)) & for V be open Subset of S st ( sup D) in V holds D meets V;

      let E be non empty directed Subset of ( Omega T);

      

       A3: ( Omega S) = ( Omega T) by A1, Th13;

      hence ex_sup_of (E,( Omega T)) by A2;

      let V be open Subset of T such that

       A4: ( sup E) in V;

      reconsider W = V as Subset of S by A1;

      W is open by A1, TOPS_3: 76;

      hence thesis by A2, A3, A4;

    end;

     Lm7:

    now

      let T be non empty 1-sorted, D be non empty Subset of T, d be Element of T such that

       A1: the carrier of T = {d};

      thus D = {d}

      proof

        thus D c= {d} by A1;

        set x = the Element of D;

        let a be object;

        assume a in {d};

        then

         A2: a = d by TARSKI:def 1;

        x in D;

        hence thesis by A1, A2, TARSKI:def 1;

      end;

    end;

    registration

      cluster trivial -> monotone-convergence for T_0-TopSpace;

      coherence

      proof

        let T be T_0-TopSpace;

        assume T is trivial;

        then

        consider d be Element of T such that

         A1: the carrier of T = {d} by TEX_1:def 1;

        reconsider d as Element of ( Omega T) by Lm1;

        let D be non empty directed Subset of ( Omega T);

        

         A2: the carrier of T = the carrier of ( Omega T) by Lm1;

        then D = {d} by A1, Lm7;

        hence ex_sup_of (D,( Omega T)) by YELLOW_0: 38;

        let V be open Subset of T;

        

         A3: {d} meets {d};

        assume ( sup D) in V;

        then V = {d} by A1, Lm7;

        hence thesis by A1, A2, A3, Lm7;

      end;

    end

    theorem :: WAYBEL25:28

    for S be monotone-convergence T_0-TopSpace, T be T_0-TopSpace st (S,T) are_homeomorphic holds T is monotone-convergence

    proof

      let S be monotone-convergence T_0-TopSpace, T be T_0-TopSpace;

      given h be Function of S, T such that

       A1: h is being_homeomorphism;

      the carrier of S = the carrier of ( Omega S) by Lm1;

      then

      reconsider f = h as Function of ( Omega S), ( Omega T) by Lm1;

      f is isomorphic by A1, Th18;

      then

       A2: ( rng f) = the carrier of ( Omega T) by WAYBEL_0: 66;

      let D be non empty directed Subset of ( Omega T);

      

       A3: (f " ) is isomorphic by A1, Th18, YELLOW14: 10;

      then (f " ) is sups-preserving by WAYBEL13: 20;

      then

       A4: (f " ) preserves_sup_of D;

      

       A5: ( rng h) = ( [#] T) by A1;

      

       A6: h is one-to-one by A1;

      

       A7: h is onto by A5, FUNCT_2:def 3;

      ((f " ) .: D) is directed by A3, YELLOW_2: 15;

      then

       A8: (f " D) is non empty directed Subset of ( Omega S) by A2, A5, A6, TOPS_2: 55;

      then ex_sup_of ((f " D),( Omega S)) by Def4;

      then ex_sup_of ((f .: (f " D)),( Omega T)) by A1, Th18, YELLOW14: 16;

      hence

       A9: ex_sup_of (D,( Omega T)) by A2, FUNCT_1: 77;

      let V be open Subset of T;

      assume ( sup D) in V;

      then ((h " ) . ( sup D)) in ((h " ) .: V) by FUNCT_2: 35;

      then ((h " ) . ( sup D)) in (h " V) by A5, A6, TOPS_2: 55;

      then ((h qua Function " ) . ( sup D)) in (h " V) by A7, A6, TOPS_2:def 4;

      then ((f " ) . ( sup D)) in (h " V) by A2, A6, A7, A5, TOPS_2:def 4;

      then ( sup ((f " ) .: D)) in (h " V) by A9, A4;

      then

       A10: ( sup (f " D)) in (h " V) by A2, A5, A6, TOPS_2: 55;

      (h " V) is open by A1, TOPGRP_1: 26;

      then (f " D) meets (h " V) by A8, A10, Def4;

      then

      consider a be object such that

       A11: a in (f " D) and

       A12: a in (h " V) by XBOOLE_0: 3;

      reconsider a as Element of S by A12;

      now

        take b = (h . a);

        thus b in D & b in V by A11, A12, FUNCT_2: 38;

      end;

      hence thesis by XBOOLE_0: 3;

    end;

    theorem :: WAYBEL25:29

    

     Th29: for S be Scott complete TopLattice holds S is monotone-convergence

    proof

      let S be Scott complete TopLattice;

      let D be non empty directed Subset of ( Omega S);

      thus ex_sup_of (D,( Omega S)) by YELLOW_0: 17;

      

       A1: ( Omega S) = the TopRelStr of S by Th15;

      then

       A2: the RelStr of ( Omega S) = the RelStr of S;

      reconsider E = D as Subset of S by A1;

      let V be open Subset of S;

      assume ( sup D) in V;

      then

       A3: ( sup E) in V by A2, YELLOW_0: 17, YELLOW_0: 26;

      E is non empty directed Subset of S by A2, WAYBEL_0: 3;

      hence thesis by A3, WAYBEL11:def 1;

    end;

    registration

      let L be complete LATTICE;

      cluster -> monotone-convergence for Scott TopAugmentation of L;

      coherence by Th29;

    end

    registration

      let L be complete LATTICE, S be Scott TopAugmentation of L;

      cluster the TopStruct of S -> monotone-convergence;

      coherence by Th27;

    end

    theorem :: WAYBEL25:30

    

     Th30: for X be monotone-convergence T_0-TopSpace holds ( Omega X) is up-complete

    proof

      let X be monotone-convergence T_0-TopSpace;

      for A be non empty directed Subset of ( Omega X) holds ex_sup_of (A,( Omega X)) by Def4;

      hence thesis by WAYBEL_0: 75;

    end;

    registration

      let X be monotone-convergence T_0-TopSpace;

      cluster ( Omega X) -> up-complete;

      coherence by Th30;

    end

    theorem :: WAYBEL25:31

    

     Th31: for X be monotone-convergence non empty TopSpace, N be eventually-directed prenet of ( Omega X) holds ex_sup_of N

    proof

      let X be monotone-convergence non empty TopSpace, N be eventually-directed prenet of ( Omega X);

      ( rng ( netmap (N,( Omega X)))) is directed by WAYBEL_2: 18;

      hence ex_sup_of (( rng the mapping of N),( Omega X)) by Def4;

    end;

    theorem :: WAYBEL25:32

    

     Th32: for X be monotone-convergence non empty TopSpace, N be eventually-directed net of ( Omega X) holds ( sup N) in ( Lim N)

    proof

      let X be monotone-convergence non empty TopSpace, N be eventually-directed net of ( Omega X);

      ( rng ( netmap (N,( Omega X)))) is directed by WAYBEL_2: 18;

      then

      reconsider D = ( rng the mapping of N) as non empty directed Subset of ( Omega X);

      for V be a_neighborhood of ( sup N) holds N is_eventually_in V

      proof

        let V be a_neighborhood of ( sup N);

        

         A1: ( Int V) c= V by TOPS_1: 16;

        

         A2: the TopStruct of X = the TopStruct of ( Omega X) by Def2;

        then

        reconsider I = ( Int V) as Subset of X;

        

         A3: I is open by A2, TOPS_3: 76;

        ( sup N) in I by CONNSP_2:def 1;

        then ( Sup the mapping of N) in I by WAYBEL_2:def 1;

        then D meets I by A3, Def4;

        then

        consider y be object such that

         A4: y in D and

         A5: y in I by XBOOLE_0: 3;

        reconsider y as Point of X by A5;

        consider x be object such that

         A6: x in ( dom the mapping of N) and

         A7: (the mapping of N . x) = y by A4, FUNCT_1:def 3;

        reconsider x as Element of N by A6;

        consider j be Element of N such that

         A8: for k be Element of N st j <= k holds (N . x) <= (N . k) by WAYBEL_0: 11;

        take j;

        let k be Element of N;

        assume j <= k;

        then (N . x) <= (N . k) by A8;

        then

        consider Y be Subset of X such that

         A9: Y = {(N . k)} and

         A10: (N . x) in ( Cl Y) by Def2;

        Y meets I by A3, A5, A7, A10, PRE_TOPC:def 7;

        then

        consider m be object such that

         A11: m in (Y /\ I) by XBOOLE_0: 4;

        m in Y by A11, XBOOLE_0:def 4;

        then

         A12: m = (N . k) by A9, TARSKI:def 1;

        m in I by A11, XBOOLE_0:def 4;

        hence thesis by A12, A1;

      end;

      hence thesis by YELLOW_6:def 15;

    end;

    theorem :: WAYBEL25:33

    

     Th33: for X be monotone-convergence non empty TopSpace, N be eventually-directed net of ( Omega X) holds N is convergent

    proof

      let X be monotone-convergence non empty TopSpace, N be eventually-directed net of ( Omega X);

      thus ( Lim N) <> {} by Th32;

    end;

    registration

      let X be monotone-convergence non empty TopSpace;

      cluster -> convergent for eventually-directed net of ( Omega X);

      coherence by Th33;

    end

    theorem :: WAYBEL25:34

    for X be non empty TopSpace st for N be eventually-directed net of ( Omega X) holds ex_sup_of N & ( sup N) in ( Lim N) holds X is monotone-convergence

    proof

      let X be non empty TopSpace such that

       A1: for N be eventually-directed net of ( Omega X) holds ex_sup_of N & ( sup N) in ( Lim N);

      let D be non empty directed Subset of ( Omega X);

      ( Net-Str D) = NetStr (# D, (the InternalRel of ( Omega X) |_2 D), (( id the carrier of ( Omega X)) | D) #) by WAYBEL17:def 4;

      then

       A2: ( rng the mapping of ( Net-Str D)) = D by YELLOW14: 2;

       ex_sup_of ( Net-Str D) by A1;

      hence ex_sup_of (D,( Omega X)) by A2;

      let V be open Subset of X such that

       A3: ( sup D) in V;

      reconsider Z = V as Subset of ( Omega X) by Lm1;

      

       A4: ( sup ( Net-Str D)) = ( Sup the mapping of ( Net-Str D)) by WAYBEL_2:def 1

      .= ( sup ( rng the mapping of ( Net-Str D)));

       the TopStruct of X = the TopStruct of ( Omega X) by Def2;

      then ( Int Z) = ( Int V) by TOPS_3: 77;

      then ( sup ( Net-Str D)) in ( Int Z) by A2, A3, A4, TOPS_1: 23;

      then

       A5: Z is a_neighborhood of ( sup ( Net-Str D)) by CONNSP_2:def 1;

      ( sup ( Net-Str D)) in ( Lim ( Net-Str D)) by A1;

      then ( Net-Str D) is_eventually_in V by A5, YELLOW_6:def 15;

      then

      consider i be Element of ( Net-Str D) such that

       A6: for j be Element of ( Net-Str D) st i <= j holds (( Net-Str D) . j) in V;

      now

        take a = (( Net-Str D) . i);

        ( dom the mapping of ( Net-Str D)) = the carrier of ( Net-Str D) by FUNCT_2:def 1;

        hence a in D by A2, FUNCT_1:def 3;

        thus a in V by A6;

      end;

      hence thesis by XBOOLE_0: 3;

    end;

    theorem :: WAYBEL25:35

    

     Th35: for X be monotone-convergence non empty TopSpace, Y be T_0-TopSpace, f be continuous Function of ( Omega X), ( Omega Y) holds f is directed-sups-preserving

    proof

      let X be monotone-convergence non empty TopSpace, Y be T_0-TopSpace, f be continuous Function of ( Omega X), ( Omega Y);

      let D be non empty directed Subset of ( Omega X);

      assume

       A1: ex_sup_of (D,( Omega X));

      set V = (( downarrow ( sup (f .: D))) ` );

      

       A2: the TopStruct of X = the TopStruct of ( Omega X) by Def2;

      then

      reconsider fV = (f " V) as Subset of X;

      ( [#] ( Omega Y)) <> {} ;

      then (f " V) is open by TOPS_2: 43;

      then

      reconsider fV as open Subset of X by A2, TOPS_3: 76;

      ( sup (f .: D)) <= ( sup (f .: D));

      then

       A3: ( sup (f .: D)) in ( downarrow ( sup (f .: D))) by WAYBEL_0: 17;

      

       A4: the TopStruct of Y = the TopStruct of ( Omega Y) by Def2;

      ex a be Element of ( Omega Y) st (f .: D) is_<=_than a & for b be Element of ( Omega Y) st (f .: D) is_<=_than b holds a <= b

      proof

        take a = (f . ( sup D));

        D is_<=_than ( sup D) by A1, YELLOW_0:def 9;

        hence (f .: D) is_<=_than a by YELLOW_2: 14;

        let b be Element of ( Omega Y) such that

         A5: for c be Element of ( Omega Y) st c in (f .: D) holds c <= b;

        reconsider Z = {b} as Subset of Y by Lm1;

        for G be Subset of Y st G is open holds a in G implies Z meets G

        proof

          let G be Subset of Y such that

           A6: G is open and

           A7: a in G;

          reconsider H = G as open Subset of ( Omega Y) by A4, A6, TOPS_3: 76;

          ( [#] ( Omega Y)) <> {} ;

          then (f " H) is open by TOPS_2: 43;

          then

           A8: (f " H) is open Subset of X by A2, TOPS_3: 76;

          ( sup D) in (f " H) by A7, FUNCT_2: 38;

          then D meets (f " H) by A8, Def4;

          then

          consider c be object such that

           A9: c in D and

           A10: c in (f " H) by XBOOLE_0: 3;

          reconsider c as Point of ( Omega X) by A9;

          

           A11: (f . c) in H by A10, FUNCT_2: 38;

          (f . c) <= b by A5, A9, FUNCT_2: 35;

          then

           A12: b in G by A11, WAYBEL_0:def 20;

          b in {b} by TARSKI:def 1;

          hence thesis by A12, XBOOLE_0: 3;

        end;

        then a in ( Cl Z) by A4, PRE_TOPC:def 7;

        hence thesis by Def2;

      end;

      hence

       A13: ex_sup_of ((f .: D),( Omega Y)) by YELLOW_0: 15;

      assume

       A14: ( sup (f .: D)) <> (f . ( sup D));

      ( sup (f .: D)) <= (f . ( sup D)) by A1, A13, WAYBEL17: 15;

      then not (f . ( sup D)) <= ( sup (f .: D)) by A14, ORDERS_2: 2;

      then not (f . ( sup D)) in ( downarrow ( sup (f .: D))) by WAYBEL_0: 17;

      then (f . ( sup D)) in V by XBOOLE_0:def 5;

      then ( sup D) in fV by FUNCT_2: 38;

      then D meets fV by Def4;

      then

      consider d be object such that

       A15: d in D and

       A16: d in fV by XBOOLE_0: 3;

      reconsider d as Element of ( Omega X) by A15;

      

       A17: (f . d) in V by A16, FUNCT_2: 38;

      (f . d) <= ( sup (f .: D)) by A13, A15, FUNCT_2: 35, YELLOW_4: 1;

      then ( sup (f .: D)) in V by A17, WAYBEL_0:def 20;

      hence contradiction by A3, XBOOLE_0:def 5;

    end;

    registration

      let X be monotone-convergence non empty TopSpace, Y be T_0-TopSpace;

      cluster continuous -> directed-sups-preserving for Function of ( Omega X), ( Omega Y);

      coherence by Th35;

    end

    theorem :: WAYBEL25:36

    

     Th36: for T be monotone-convergence T_0-TopSpace, R be T_0-TopSpace st R is_Retract_of T holds R is monotone-convergence

    proof

      let T be monotone-convergence T_0-TopSpace, R be T_0-TopSpace;

      given c be continuous Function of R, T, r be continuous Function of T, R such that

       A1: (r * c) = ( id R);

      let D be non empty directed Subset of ( Omega R);

      

       A2: the TopStruct of R = the TopStruct of ( Omega R) by Def2;

      then

      reconsider DR = D as non empty Subset of R;

      

       A3: the TopStruct of T = the TopStruct of ( Omega T) by Def2;

      then

      reconsider f = (c * r) as Function of ( Omega T), ( Omega T);

      reconsider rr = r as Function of ( Omega T), ( Omega R) by A3, A2;

      

       A4: (r .: (c .: D)) = ((r * c) .: DR) by RELAT_1: 126

      .= D by A1, FUNCT_1: 92;

      reconsider cc = c as Function of ( Omega R), ( Omega T) by A3, A2;

      cc is continuous by A3, A2, YELLOW12: 36;

      then

       A5: (cc .: D) is directed by YELLOW_2: 15;

      then

       A6: ex_sup_of ((cc .: D),( Omega T)) by Def4;

      f is continuous by A3, YELLOW12: 36;

      then

       A7: f preserves_sup_of (cc .: D) by A5, WAYBEL_0:def 37;

      rr is continuous by A3, A2, YELLOW12: 36;

      then

       A8: rr preserves_sup_of (cc .: D) by A5, WAYBEL_0:def 37;

      hence ex_sup_of (D,( Omega R)) by A6, A4;

      

       A9: (c . ( sup D)) = (c . (r . ( sup (cc .: D)))) by A6, A4, A8

      .= (f . ( sup (cc .: D))) by A3, FUNCT_2: 15

      .= ( sup (f .: (cc .: D))) by A6, A7

      .= ( sup (cc .: D)) by A4, RELAT_1: 126;

      let V be open Subset of R;

      assume ( sup D) in V;

      then

       A10: (c . ( sup D)) in (c .: V) by FUNCT_2: 35;

      

       A11: (c .: V) c= (r " V)

      proof

        let a be object;

        assume a in (c .: V);

        then

        consider x be object such that

         A12: x in the carrier of R and

         A13: x in V and

         A14: a = (c . x) by FUNCT_2: 64;

        reconsider x as Point of R by A12;

        

         A15: a = (c . x) by A14;

        (r . a) = ((r * c) . x) by A14, FUNCT_2: 15

        .= x by A1;

        hence thesis by A13, A15, FUNCT_2: 38;

      end;

      ( [#] R) <> {} ;

      then (r " V) is open by TOPS_2: 43;

      then (c .: D) meets (r " V) by A5, A11, A9, A10, Def4;

      then

      consider d be object such that

       A16: d in (cc .: D) and

       A17: d in (r " V) by XBOOLE_0: 3;

      now

        take a = (r . d);

        thus a in D by A4, A16, FUNCT_2: 35;

        thus a in V by A17, FUNCT_2: 38;

      end;

      hence thesis by XBOOLE_0: 3;

    end;

    theorem :: WAYBEL25:37

    

     Th37: for T be injective T_0-TopSpace, S be Scott TopAugmentation of ( Omega T) holds the TopStruct of S = the TopStruct of T

    proof

      set SS = Sierpinski_Space , B = ( BoolePoset { 0 });

      let T be injective T_0-TopSpace, S be Scott TopAugmentation of ( Omega T);

      consider M be non empty set such that

       A1: T is_Retract_of ( product (M --> SS)) by WAYBEL18: 19;

      consider c be continuous Function of T, ( product (M --> SS)), r be continuous Function of ( product (M --> SS)), T such that

       A2: (r * c) = ( id T) by A1;

      

       A3: the TopStruct of T = the TopStruct of ( Omega T) by Def2;

      

       A4: the TopStruct of ( product (M --> SS)) = the TopStruct of ( Omega ( product (M --> SS))) by Def2;

      then

      reconsider c1a = c as Function of ( Omega T), ( Omega ( product (M --> SS))) by A3;

      set S2M = the Scott TopAugmentation of ( product (M --> B));

      

       A5: the TopStruct of S = the TopStruct of S;

      

       A6: the RelStr of S2M = the RelStr of ( product (M --> B)) by YELLOW_9:def 4;

      then

      reconsider c1 = c as Function of ( Omega T), ( product (M --> B)) by A3, Th3;

      

       A7: the RelStr of S = the RelStr of ( Omega T) by YELLOW_9:def 4;

      then

      reconsider c2 = c1 as Function of S, S2M by A6;

      

       A8: the carrier of S2M = the carrier of ( product (M --> SS)) by Th3;

      then

      reconsider rr = r as Function of S2M, T;

      

       A9: the topology of S2M = the topology of ( product (M --> SS)) by WAYBEL18: 15;

      then

      reconsider W = T as monotone-convergence non empty TopSpace by A1, A8, Th36;

      ( Omega ( product (M --> SS))) = ( Omega S2M) by A9, A8, Th13;

      

      then

       A10: the RelStr of ( Omega ( product (M --> SS))) = the RelStr of ( product (M --> B)) by Th16

      .= the RelStr of S2M by YELLOW_9:def 4;

      reconsider r1 = r as Function of ( product (M --> B)), ( Omega T) by A8, A6, A3;

      

       A11: the RelStr of ( Omega S2M) = the RelStr of ( product (M --> B)) by Th16;

      then

      reconsider rr1 = r1 as Function of ( Omega S2M), ( Omega T);

      reconsider r2 = r1 as Function of S2M, S by A6, A7;

      reconsider r3 = r2 as Function of ( product (M --> SS)), S by Th3;

       the TopStruct of ( Omega S2M) = the TopStruct of S2M by Def2;

      then rr1 is continuous by A9, A8, A3, YELLOW12: 36;

      then r2 is directed-sups-preserving by A6, A7, A11, WAYBEL21: 6;

      then r3 is continuous by A9, A8, A5, YELLOW12: 36;

      then

       A12: (r3 * c) is continuous;

      reconsider c1a as continuous Function of ( Omega W), ( Omega ( product (M --> SS))) by A3, A4, YELLOW12: 36;

      c2 = c1a;

      then

       A13: c2 is directed-sups-preserving by A7, A10, WAYBEL21: 6;

       the TopStruct of T = the TopStruct of T;

      then rr is continuous by A9, A8, YELLOW12: 36;

      then (rr * c2) is continuous by A13;

      hence thesis by A2, A12, YELLOW14: 33;

    end;

    theorem :: WAYBEL25:38

    for T be injective T_0-TopSpace holds T is compact locally-compact sober

    proof

      let T be injective T_0-TopSpace;

      set S = the Scott TopAugmentation of ( Omega T);

      

       A1: S is compact locally-compact sober by WAYBEL14: 32;

       the TopStruct of S = the TopStruct of T by Th37;

      hence thesis by A1, YELLOW14: 26, YELLOW14: 27, YELLOW14: 28;

    end;

    theorem :: WAYBEL25:39

    

     Th39: for T be injective T_0-TopSpace holds T is monotone-convergence

    proof

      let T be injective T_0-TopSpace;

      set S = the Scott TopAugmentation of ( Omega T);

       the TopStruct of S = the TopStruct of T by Th37;

      hence thesis by Th27;

    end;

    registration

      cluster injective -> monotone-convergence for T_0-TopSpace;

      coherence by Th39;

    end

    theorem :: WAYBEL25:40

    

     Th40: for X be non empty TopSpace, Y be monotone-convergence T_0-TopSpace, N be net of ( ContMaps (X,( Omega Y))), f,g be Function of X, ( Omega Y) st f = ( "\/" (( rng the mapping of N),(( Omega Y) |^ the carrier of X))) & ex_sup_of (( rng the mapping of N),(( Omega Y) |^ the carrier of X)) & g in ( rng the mapping of N) holds g <= f

    proof

      let X be non empty TopSpace, Y be monotone-convergence T_0-TopSpace, N be net of ( ContMaps (X,( Omega Y))), f,g be Function of X, ( Omega Y);

      set m = the mapping of N, L = (( Omega Y) |^ the carrier of X), s = ( "\/" (( rng m),L));

      assume that

       A1: f = ( "\/" (( rng the mapping of N),(( Omega Y) |^ the carrier of X))) and

       A2: ex_sup_of (( rng m),L) and

       A3: g in ( rng the mapping of N);

      reconsider g1 = g as Element of L by WAYBEL24: 19;

      ( rng m) is_<=_than s by A2, YELLOW_0:def 9;

      then g1 <= s by A3;

      hence thesis by A1, WAYBEL10: 11;

    end;

    theorem :: WAYBEL25:41

    

     Th41: for X be non empty TopSpace, Y be monotone-convergence T_0-TopSpace, N be net of ( ContMaps (X,( Omega Y))), x be Point of X, f be Function of X, ( Omega Y) st (for a be Point of X holds ( commute (N,a,( Omega Y))) is eventually-directed) & f = ( "\/" (( rng the mapping of N),(( Omega Y) |^ the carrier of X))) holds (f . x) = ( sup ( commute (N,x,( Omega Y))))

    proof

      let X be non empty TopSpace, Y be monotone-convergence T_0-TopSpace, N be net of ( ContMaps (X,( Omega Y))), x be Point of X, f be Function of X, ( Omega Y) such that

       A1: for a be Point of X holds ( commute (N,a,( Omega Y))) is eventually-directed and

       A2: f = ( "\/" (( rng the mapping of N),(( Omega Y) |^ the carrier of X)));

      set n = the mapping of N, m = the mapping of ( commute (N,x,( Omega Y))), L = (( Omega Y) |^ the carrier of X);

      

       A3: for x be Point of X holds ex_sup_of ( commute (N,x,( Omega Y)))

      proof

        let x be Point of X;

        ( commute (N,x,( Omega Y))) is eventually-directed by A1;

        hence thesis by Th31;

      end;

      then

       A4: ex_sup_of (( rng n),L) by Th26;

      

       A5: ( dom n) = the carrier of N by FUNCT_2:def 1;

      then

       A6: ( dom m) = the carrier of N by Lm6;

      

       A7: for a be Element of ( Omega Y) st ( rng m) is_<=_than a holds (f . x) <= a

      proof

        let a be Element of ( Omega Y);

        defpred P[ set, set] means ($1 = x implies $2 = a) & ($1 <> x implies ex u be Element of X st $1 = u & $2 = ( sup ( commute (N,u,( Omega Y)))));

        

         A8: ( Omega Y) = ((the carrier of X --> ( Omega Y)) . x);

        

         A9: for e be Element of X holds ex u be Element of ( Omega Y) st P[e, u]

        proof

          let e be Element of X;

          per cases ;

            suppose e = x;

            hence thesis;

          end;

            suppose

             A10: e <> x;

            reconsider e as Element of X;

            take ( sup ( commute (N,e,( Omega Y))));

            thus thesis by A10;

          end;

        end;

        consider t be Function of the carrier of X, the carrier of ( Omega Y) such that

         A11: for u be Element of X holds P[u, (t . u)] from FUNCT_2:sch 3( A9);

        reconsider t as Function of X, ( Omega Y);

        reconsider tt = t as Element of L by WAYBEL24: 19;

        reconsider p = ( "\/" (( rng n),L)), q = tt as Element of ( product (the carrier of X --> ( Omega Y))) by YELLOW_1:def 5;

        assume

         A12: for e be Element of ( Omega Y) st e in ( rng m) holds e <= a;

        tt is_>=_than ( rng n)

        proof

          let s be Element of L;

          reconsider ss = s as Function of X, ( Omega Y) by WAYBEL24: 19;

          reconsider s9 = s, t9 = tt as Element of ( product (the carrier of X --> ( Omega Y))) by YELLOW_1:def 5;

          assume s in ( rng n);

          then

          consider i be object such that

           A13: i in ( dom n) and

           A14: s = (n . i) by FUNCT_1:def 3;

          reconsider i as Point of N by A13;

          

           A15: for j be Element of X holds (s9 . j) <= (t9 . j)

          proof

            let j be Element of X;

            

             A17: (ss . j) = (the mapping of ( commute (N,j,( Omega Y))) . i) by A14, Th24;

            per cases ;

              suppose j <> x;

              then ex u be Element of X st j = u & (t . j) = ( sup ( commute (N,u,( Omega Y)))) by A11;

              

              then

               A18: (t9 . j) = ( Sup the mapping of ( commute (N,j,( Omega Y)))) by WAYBEL_2:def 1

              .= ( sup ( rng the mapping of ( commute (N,j,( Omega Y)))));

              ( commute (N,j,( Omega Y))) is eventually-directed by A1;

              then ex_sup_of ( commute (N,j,( Omega Y))) by Th31;

              then

               A19: ex_sup_of (( rng the mapping of ( commute (N,j,( Omega Y)))),( Omega Y));

              i in ( dom the mapping of ( commute (N,j,( Omega Y)))) by A13, Lm6;

              then (ss . j) in ( rng the mapping of ( commute (N,j,( Omega Y)))) by A17, FUNCT_1:def 3;

              hence thesis by A18, A19, YELLOW_4: 1;

            end;

              suppose

               A20: j = x;

              

               A21: (m . i) in ( rng m) by A6, FUNCT_1:def 3;

              (ss . x) = (m . i) by A14, Th24;

              then (ss . x) <= a by A12, A21;

              hence thesis by A11, A20;

            end;

          end;

          L = ( product (the carrier of X --> ( Omega Y))) by YELLOW_1:def 5;

          hence s <= tt by A15, WAYBEL_3: 28;

        end;

        then ( "\/" (( rng n),L)) <= tt by A4, YELLOW_0: 30;

        then

         A22: p <= q by YELLOW_1:def 5;

        (tt . x) = a by A11;

        hence thesis by A2, A8, A22, WAYBEL_3: 28;

      end;

      ( rng m) is_<=_than (f . x)

      proof

        let w be Element of ( Omega Y);

        assume w in ( rng m);

        then

        consider i be object such that

         A23: i in ( dom m) and

         A24: (m . i) = w by FUNCT_1:def 3;

        reconsider i as Point of N by A5, A23, Lm6;

        reconsider g = (n . i) as Function of X, ( Omega Y) by Lm5;

        g in ( rng n) by A5, FUNCT_1:def 3;

        then g <= f by A2, A3, Th26, Th40;

        then ex a,b be Element of ( Omega Y) st a = (g . x) & b = (f . x) & a <= b;

        hence w <= (f . x) by A24, Th24;

      end;

      

      hence (f . x) = ( Sup the mapping of ( commute (N,x,( Omega Y)))) by A7, YELLOW_0: 30

      .= ( sup ( commute (N,x,( Omega Y)))) by WAYBEL_2:def 1;

    end;

    theorem :: WAYBEL25:42

    

     Th42: for X be non empty TopSpace, Y be monotone-convergence T_0-TopSpace, N be net of ( ContMaps (X,( Omega Y))) st for x be Point of X holds ( commute (N,x,( Omega Y))) is eventually-directed holds ( "\/" (( rng the mapping of N),(( Omega Y) |^ the carrier of X))) is continuous Function of X, Y

    proof

      let X be non empty TopSpace, Y be monotone-convergence T_0-TopSpace, N be net of ( ContMaps (X,( Omega Y))) such that

       A1: for x be Point of X holds ( commute (N,x,( Omega Y))) is eventually-directed;

      set m = the mapping of N, L = (( Omega Y) |^ the carrier of X);

      reconsider fo = ( "\/" (( rng m),L)) as Function of X, ( Omega Y) by WAYBEL24: 19;

      

       A2: the TopStruct of Y = the TopStruct of ( Omega Y) by Def2;

      then

      reconsider f = fo as Function of X, Y;

      

       A3: ( dom m) = the carrier of N by FUNCT_2:def 1;

      

       A4: for V be Subset of Y st V is open holds (f " V) is open

      proof

        let V be Subset of Y such that

         A5: V is open;

        set M = { A where A be Subset of X : ex i be Element of N, g be Function of X, ( Omega Y) st g = (N . i) & A = (g " V) };

        for x be object holds x in (f " V) iff x in ( union M)

        proof

          let x be object;

          

           A6: ( dom f) = the carrier of X by FUNCT_2:def 1;

          thus x in (f " V) implies x in ( union M)

          proof

            

             A7: m in ( Funcs (the carrier of N,( Funcs (the carrier of X,the carrier of Y)))) by Lm4;

            assume

             A8: x in (f " V);

            then

             A9: (f . x) in V by FUNCT_2: 38;

            reconsider x as Point of X by A8;

            set NET = ( commute (N,x,( Omega Y)));

            NET is eventually-directed by A1;

            then

            reconsider W = ( rng ( netmap (NET,( Omega Y)))) as non empty directed Subset of ( Omega Y) by WAYBEL_2: 18;

            (f . x) = ( sup NET) by A1, Th41

            .= ( Sup the mapping of NET) by WAYBEL_2:def 1

            .= ( sup W);

            then W meets V by A5, A9, Def4;

            then

            consider k be object such that

             A10: k in W and

             A11: k in V by XBOOLE_0: 3;

            consider i be object such that

             A12: i in ( dom ( netmap (NET,( Omega Y)))) and

             A13: k = (( netmap (NET,( Omega Y))) . i) by A10, FUNCT_1:def 3;

            ( ContMaps (X,( Omega Y))) is SubRelStr of (( Omega Y) |^ the carrier of X) by WAYBEL24:def 3;

            then

             A14: the carrier of ( ContMaps (X,( Omega Y))) c= the carrier of (( Omega Y) |^ the carrier of X) by YELLOW_0:def 13;

            then the RelStr of NET = the RelStr of N by Def3;

            then

            reconsider i as Element of N by A12;

            reconsider g = (N . i) as Function of X, ( Omega Y) by WAYBEL24: 21;

            

             A15: ( dom g) = the carrier of X by FUNCT_2:def 1;

            

             A16: (g " V) in M;

            (( netmap (NET,( Omega Y))) . i) = ((( commute the mapping of N) . x) . i) by A14, Def3

            .= ((the mapping of N . i) . x) by A7, FUNCT_6: 56;

            then x in (g " V) by A11, A13, A15, FUNCT_1:def 7;

            hence thesis by A16, TARSKI:def 4;

          end;

          assume x in ( union M);

          then

          consider Z be set such that

           A17: x in Z and

           A18: Z in M by TARSKI:def 4;

          consider A be Subset of X such that

           A19: Z = A and

           A20: ex i be Element of N, g be Function of X, ( Omega Y) st g = (N . i) & A = (g " V) by A18;

          consider i be Element of N, g be Function of X, ( Omega Y) such that

           A21: g = (N . i) and

           A22: A = (g " V) by A20;

          

           A23: (g . x) in V by A17, A19, A22, FUNCT_1:def 7;

          

           A24: for x be Point of X holds ex_sup_of ( commute (N,x,( Omega Y)))

          proof

            let x be Point of X;

            ( commute (N,x,( Omega Y))) is eventually-directed by A1;

            hence thesis by Th31;

          end;

          reconsider x as Element of X by A17, A19;

          (m . i) in ( rng m) by A3, FUNCT_1:def 3;

          then g <= fo by A21, A24, Th26, Th40;

          then ex a,b be Element of ( Omega Y) st a = (g . x) & b = (fo . x) & a <= b;

          then

          consider O be Subset of Y such that

           A25: O = {(f . x)} and

           A26: (g . x) in ( Cl O) by Def2;

          V meets O by A5, A23, A26, PRE_TOPC:def 7;

          then

          consider w be object such that

           A27: w in (V /\ O) by XBOOLE_0: 4;

          w in O by A27, XBOOLE_0:def 4;

          then

           A28: w = (f . x) by A25, TARSKI:def 1;

          w in V by A27, XBOOLE_0:def 4;

          hence thesis by A6, A28, FUNCT_1:def 7;

        end;

        then

         A29: (f " V) = ( union M) by TARSKI: 2;

        M c= ( bool the carrier of X)

        proof

          let m be object;

          assume m in M;

          then ex A be Subset of X st m = A & ex i be Element of N, g be Function of X, ( Omega Y) st g = (N . i) & A = (g " V);

          hence thesis;

        end;

        then

        reconsider M as Subset-Family of X;

        reconsider M as Subset-Family of X;

        M is open

        proof

          let P be Subset of X;

          assume P in M;

          then

          consider A be Subset of X such that

           A30: P = A and

           A31: ex i be Element of N, g be Function of X, ( Omega Y) st g = (N . i) & A = (g " V);

          consider i be Element of N, g be Function of X, ( Omega Y) such that

           A32: g = (N . i) and

           A33: A = (g " V) by A31;

          consider g9 be Function of X, ( Omega Y) such that

           A34: g = g9 and

           A35: g9 is continuous by A32, WAYBEL24:def 3;

           the TopStruct of X = the TopStruct of X;

          then

          reconsider g99 = g9 as continuous Function of X, Y by A2, A35, YELLOW12: 36;

          ( [#] Y) <> {} ;

          then (g99 " V) is open by A5, TOPS_2: 43;

          hence thesis by A30, A33, A34;

        end;

        hence thesis by A29, TOPS_2: 19;

      end;

      ( [#] Y) <> {} ;

      hence thesis by A4, TOPS_2: 43;

    end;

    theorem :: WAYBEL25:43

    for X be non empty TopSpace, Y be monotone-convergence T_0-TopSpace holds ( ContMaps (X,( Omega Y))) is directed-sups-inheriting SubRelStr of (( Omega Y) |^ the carrier of X)

    proof

      let X be non empty TopSpace, Y be monotone-convergence T_0-TopSpace;

      set L = (( Omega Y) |^ the carrier of X);

      reconsider C = ( ContMaps (X,( Omega Y))) as non empty full SubRelStr of L by WAYBEL24:def 3;

      C is directed-sups-inheriting

      proof

        let D be directed Subset of C such that

         A1: D <> {} and ex_sup_of (D,L);

        reconsider D as non empty directed Subset of C by A1;

        set N = ( Net-Str D);

        

         A2: the TopStruct of X = the TopStruct of X;

        for x be Point of X holds ( commute (N,x,( Omega Y))) is eventually-directed;

        then

         A3: ( "\/" (( rng the mapping of N),(( Omega Y) |^ the carrier of X))) is continuous Function of X, Y by Th42;

         the TopStruct of Y = the TopStruct of ( Omega Y) by Def2;

        then ( "\/" (( rng the mapping of N),(( Omega Y) |^ the carrier of X))) is continuous Function of X, ( Omega Y) by A2, A3, YELLOW12: 36;

        then

         A4: ( "\/" (( rng the mapping of N),(( Omega Y) |^ the carrier of X))) in the carrier of C by WAYBEL24:def 3;

        ( Net-Str D) = NetStr (# D, (the InternalRel of C |_2 D), (( id the carrier of C) | D) #) by WAYBEL17:def 4;

        hence thesis by A4, YELLOW14: 2;

      end;

      hence thesis;

    end;