waybel21.miz



    begin

    definition

      let S,T be Semilattice;

      :: WAYBEL21:def1

      mode SemilatticeHomomorphism of S,T -> Function of S, T means

      : Def1: for X be finite Subset of S holds it preserves_inf_of X;

      existence

      proof

        reconsider f = (the carrier of S --> ( Top T)) as Function of S, T;

        take f;

        let X be finite Subset of S such that

         A2: ex_inf_of (X,S);

        per cases ;

          suppose

           A3: X = {} ;

          then

           A4: (f .: X) = {} ;

          hence ex_inf_of ((f .: X),T) by A1, A2, A3, WAYBEL20: 5, YELLOW_0: 43;

          thus (f . ( inf X)) = ( inf (f .: X)) by A4, FUNCOP_1: 7;

        end;

          suppose X <> {} ;

          then

          reconsider A = X as non empty Subset of S;

          set a = the Element of A;

          reconsider a as Element of S;

          

           A5: ( dom f) = the carrier of S by FUNCOP_1: 13;

          (f . a) = ( Top T) by FUNCOP_1: 7;

          then ( Top T) in (f .: X) by A5, FUNCT_1:def 6;

          then

           A6: {( Top T)} c= (f .: X) by ZFMISC_1: 31;

          (f .: X) c= {( Top T)} by FUNCOP_1: 81;

          then

           A7: {( Top T)} = (f .: X) by A6;

          (f . ( inf X)) = ( Top T) by FUNCOP_1: 7;

          hence thesis by A7, YELLOW_0: 38, YELLOW_0: 39;

        end;

      end;

    end

    registration

      let S,T be Semilattice;

      cluster meet-preserving -> monotone for Function of S, T;

      coherence

      proof

        let f be Function of S, T;

        assume

         A1: f is meet-preserving;

        let x,y be Element of S;

        assume x <= y;

        then x = (x "/\" y) by YELLOW_0: 25;

        then (f . x) = ((f . x) "/\" (f . y)) by A1, WAYBEL_6: 1;

        hence thesis by YELLOW_0: 25;

      end;

    end

    registration

      let S be Semilattice, T be upper-bounded Semilattice;

      cluster -> meet-preserving for SemilatticeHomomorphism of S, T;

      coherence by Def1;

    end

    theorem :: WAYBEL21:1

    for S,T be upper-bounded Semilattice holds for f be SemilatticeHomomorphism of S, T holds (f . ( Top S)) = ( Top T)

    proof

      let S,T be upper-bounded Semilattice;

      let f be SemilatticeHomomorphism of S, T;

      

       A1: f preserves_inf_of ( {} S) by Def1;

       ex_inf_of (( {} S),S) by YELLOW_0: 43;

      then (f . ( inf ( {} S))) = ( inf (f .: ( {} S))) by A1;

      hence thesis;

    end;

    theorem :: WAYBEL21:2

    

     Th2: for S,T be Semilattice, f be Function of S, T st f is meet-preserving holds for X be finite non empty Subset of S holds f preserves_inf_of X

    proof

      let S,T be Semilattice, f be Function of S, T such that

       A1: f is meet-preserving;

      let X be finite non empty Subset of S such that ex_inf_of (X,S);

      

       A2: X is finite;

      defpred P[ set] means $1 <> {} implies ex_inf_of ($1,S) & ex_inf_of ((f .: $1),T) & ( inf (f .: $1)) = (f . ( "/\" ($1,S)));

      

       A3: P[ {} ];

       A4:

      now

        let y,x be set such that

         A5: y in X and x c= X and

         A6: P[x];

        thus P[(x \/ {y})]

        proof

          assume (x \/ {y}) <> {} ;

          reconsider y9 = y as Element of S by A5;

          set fy = (f . y9);

          

           A7: ex_inf_of ( {fy},T) by YELLOW_0: 38;

          

           A8: ( inf {fy}) = fy by YELLOW_0: 39;

          

           A9: ex_inf_of ( {y9},S) by YELLOW_0: 38;

          

           A10: ( inf {y9}) = y by YELLOW_0: 39;

          thus ex_inf_of ((x \/ {y}),S) by A6, A9, YELLOW_2: 4;

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

          then

           A11: ( Im (f,y)) = {fy} by FUNCT_1: 59;

          then

           A12: (f .: (x \/ {y})) = ((f .: x) \/ {fy}) by RELAT_1: 120;

          hence ex_inf_of ((f .: (x \/ {y})),T) by A6, A7, A11, YELLOW_2: 4;

          per cases ;

            suppose x = {} ;

            hence thesis by A8, A11, YELLOW_0: 39;

          end;

            suppose

             A13: x <> {} ;

            

            hence ( "/\" ((f .: (x \/ {y})),T)) = ((f . ( "/\" (x,S))) "/\" fy) by A6, A7, A8, A12, YELLOW_2: 4

            .= (f . (( "/\" (x,S)) "/\" y9)) by A1, WAYBEL_6: 1

            .= (f . ( "/\" ((x \/ {y}),S))) by A6, A9, A10, A13, YELLOW_2: 4;

          end;

        end;

      end;

       P[X] from FINSET_1:sch 2( A2, A3, A4);

      hence thesis;

    end;

    theorem :: WAYBEL21:3

    for S,T be upper-bounded Semilattice, f be meet-preserving Function of S, T st (f . ( Top S)) = ( Top T) holds f is SemilatticeHomomorphism of S, T

    proof

      let S,T be upper-bounded Semilattice, f be meet-preserving Function of S, T such that

       A1: (f . ( Top S)) = ( Top T);

      thus S is upper-bounded implies T is upper-bounded;

      let X be finite Subset of S;

      

       A2: ex_inf_of ((f .: {} ),T) by YELLOW_0: 43;

      X = {} or f preserves_inf_of X by Th2;

      hence thesis by A1, A2;

    end;

    theorem :: WAYBEL21:4

    

     Th4: for S,T be Semilattice, f be Function of S, T st f is meet-preserving & for X be filtered non empty Subset of S holds f preserves_inf_of X holds for X be non empty Subset of S holds f preserves_inf_of X

    proof

      let S,T be Semilattice, f be Function of S, T such that

       A1: f is meet-preserving and

       A2: for X be non empty filtered Subset of S holds f preserves_inf_of X;

      let X be non empty Subset of S such that

       A3: ex_inf_of (X,S);

      defpred P[ object] means ex Y be non empty finite Subset of X st ex_inf_of (Y,S) & $1 = ( "/\" (Y,S));

      consider Z be set such that

       A4: for x be object holds x in Z iff x in the carrier of S & P[x] from XBOOLE_0:sch 1;

      set a = the Element of X;

      reconsider a9 = a as Element of S;

      

       A5: ex_inf_of ( {a},S) by YELLOW_0: 38;

      

       A6: ( inf {a9}) = a by YELLOW_0: 39;

      Z c= the carrier of S by A4;

      then

      reconsider Z as non empty Subset of S by A4, A5, A6;

       A7:

      now

        let Y be finite Subset of X;

        Y is Subset of S by XBOOLE_1: 1;

        hence Y <> {} implies ex_inf_of (Y,S) by YELLOW_0: 55;

      end;

       A8:

      now

        let Y be finite Subset of X;

        reconsider Y9 = Y as Subset of S by XBOOLE_1: 1;

        assume

         A9: Y <> {} ;

        then ex_inf_of (Y9,S) by YELLOW_0: 55;

        hence ( "/\" (Y,S)) in Z by A4, A9;

      end;

       A10:

      now

        let x be Element of S;

        assume x in Z;

        then ex Y be non empty finite Subset of X st ex_inf_of (Y,S) & x = ( "/\" (Y,S)) by A4;

        hence ex Y be finite Subset of X st ex_inf_of (Y,S) & x = ( "/\" (Y,S));

      end;

      then

       A11: Z is filtered by A7, A8, WAYBEL_0: 56;

      

       A12: ex_inf_of (Z,S) by A3, A7, A8, A10, WAYBEL_0: 58;

      

       A13: f preserves_inf_of Z by A2, A11;

      then

       A14: ex_inf_of ((f .: Z),T) by A12;

      

       A15: ( inf (f .: Z)) = (f . ( inf Z)) by A12, A13;

      

       A16: ( inf Z) = ( inf X) by A3, A7, A8, A10, WAYBEL_0: 59;

      X c= Z

      proof

        let x be object;

        assume

         A17: x in X;

        then

        reconsider Y = {x} as finite Subset of X by ZFMISC_1: 31;

        reconsider x as Element of S by A17;

        Y is Subset of S by XBOOLE_1: 1;

        then

         A18: ex_inf_of (Y,S) by YELLOW_0: 55;

        x = ( "/\" (Y,S)) by YELLOW_0: 39;

        hence thesis by A4, A18;

      end;

      then

       A19: (f .: X) c= (f .: Z) by RELAT_1: 123;

      

       A20: (f .: Z) is_>=_than (f . ( inf X)) by A14, A15, A16, YELLOW_0: 31;

      

       A21: (f .: X) is_>=_than (f . ( inf X)) by A19, A20;

       A22:

      now

        let b be Element of T;

        assume

         A23: (f .: X) is_>=_than b;

        (f .: Z) is_>=_than b

        proof

          let a be Element of T;

          assume a in (f .: Z);

          then

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

           A24: x in Z and

           A25: a = (f . x) by FUNCT_1:def 6;

          consider Y be non empty finite Subset of X such that

           A26: ex_inf_of (Y,S) and

           A27: x = ( "/\" (Y,S)) by A4, A24;

          reconsider Y as Subset of S by XBOOLE_1: 1;

          

           A28: (f .: Y) c= (f .: X) by RELAT_1: 123;

          

           A29: f preserves_inf_of Y by A1, Th2;

          

           A30: b is_<=_than (f .: Y) by A23, A28;

          

           A31: a = ( "/\" ((f .: Y),T)) by A25, A26, A27, A29;

           ex_inf_of ((f .: Y),T) by A26, A29;

          hence thesis by A30, A31, YELLOW_0:def 10;

        end;

        hence (f . ( inf X)) >= b by A14, A15, A16, YELLOW_0: 31;

      end;

      hence ex_inf_of ((f .: X),T) by A21, YELLOW_0: 16;

      hence ( inf (f .: X)) = (f . ( inf X)) by A21, A22, YELLOW_0:def 10;

    end;

    theorem :: WAYBEL21:5

    

     Th5: for S,T be Semilattice, f be Function of S, T st f is infs-preserving holds f is SemilatticeHomomorphism of S, T

    proof

      let S,T be Semilattice, f be Function of S, T such that

       A1: f is infs-preserving;

      reconsider e = {} as Subset of S by XBOOLE_1: 2;

      hereby

        assume S is upper-bounded;

        then

         A2: ex_inf_of (e,S) by YELLOW_0: 43;

        f preserves_inf_of e by A1;

        then

         A3: ex_inf_of ((f .: e),T) by A2;

        (f .: e) = {} ;

        hence T is upper-bounded by A3, WAYBEL20: 5;

      end;

      let X be finite Subset of S;

      thus thesis by A1;

    end;

    theorem :: WAYBEL21:6

    

     Th6: for S1,T1,S2,T2 be non empty RelStr st the RelStr of S1 = the RelStr of S2 & the RelStr of T1 = the RelStr of T2 holds for f1 be Function of S1, T1, f2 be Function of S2, T2 st f1 = f2 holds (f1 is infs-preserving implies f2 is infs-preserving) & (f1 is directed-sups-preserving implies f2 is directed-sups-preserving)

    proof

      let S1,T1,S2,T2 be non empty RelStr such that

       A1: the RelStr of S1 = the RelStr of S2 and

       A2: the RelStr of T1 = the RelStr of T2;

      let f1 be Function of S1, T1, f2 be Function of S2, T2 such that

       A3: f1 = f2;

      thus f1 is infs-preserving implies f2 is infs-preserving by A1, A2, A3, WAYBEL_0: 65;

      assume

       A4: for X be Subset of S1 st X is non empty directed holds f1 preserves_sup_of X;

      let X be Subset of S2;

      reconsider Y = X as Subset of S1 by A1;

      assume X is non empty directed;

      then f1 preserves_sup_of Y by A1, A4, WAYBEL_0: 3;

      hence thesis by A1, A2, A3, WAYBEL_0: 65;

    end;

    theorem :: WAYBEL21:7

    for S1,T1,S2,T2 be non empty RelStr st the RelStr of S1 = the RelStr of S2 & the RelStr of T1 = the RelStr of T2 holds for f1 be Function of S1, T1, f2 be Function of S2, T2 st f1 = f2 holds (f1 is sups-preserving implies f2 is sups-preserving) & (f1 is filtered-infs-preserving implies f2 is filtered-infs-preserving)

    proof

      let S1,T1,S2,T2 be non empty RelStr such that

       A1: the RelStr of S1 = the RelStr of S2 and

       A2: the RelStr of T1 = the RelStr of T2;

      let f1 be Function of S1, T1, f2 be Function of S2, T2 such that

       A3: f1 = f2;

      thus f1 is sups-preserving implies f2 is sups-preserving by A1, A2, A3, WAYBEL_0: 65;

      assume

       A4: for X be Subset of S1 st X is non empty filtered holds f1 preserves_inf_of X;

      let X be Subset of S2;

      reconsider Y = X as Subset of S1 by A1;

      assume X is non empty filtered;

      then f1 preserves_inf_of Y by A1, A4, WAYBEL_0: 4;

      hence thesis by A1, A2, A3, WAYBEL_0: 65;

    end;

    theorem :: WAYBEL21:8

    

     Th8: for T be complete LATTICE holds for S be infs-inheriting full non empty SubRelStr of T holds ( incl (S,T)) is infs-preserving

    proof

      let T be complete LATTICE;

      let S be infs-inheriting full non empty SubRelStr of T;

      set f = ( incl (S,T));

      let X be Subset of S;

      assume ex_inf_of (X,S);

      thus ex_inf_of ((f .: X),T) by YELLOW_0: 17;

      the carrier of S c= the carrier of T by YELLOW_0:def 13;

      then

       A1: f = ( id the carrier of S) by YELLOW_9:def 1;

      then

       A2: (f .: X) = X by FUNCT_1: 92;

      

       A3: ex_inf_of (X,T) by YELLOW_0: 17;

      

       A4: (f . ( inf X)) = ( inf X) by A1;

      ( "/\" (X,T)) in the carrier of S by A3, YELLOW_0:def 18;

      hence thesis by A2, A3, A4, YELLOW_0: 63;

    end;

    theorem :: WAYBEL21:9

    for T be complete LATTICE holds for S be sups-inheriting full non empty SubRelStr of T holds ( incl (S,T)) is sups-preserving

    proof

      let T be complete LATTICE;

      let S be sups-inheriting full non empty SubRelStr of T;

      set f = ( incl (S,T));

      let X be Subset of S;

      assume ex_sup_of (X,S);

      thus ex_sup_of ((f .: X),T) by YELLOW_0: 17;

      the carrier of S c= the carrier of T by YELLOW_0:def 13;

      then

       A1: f = ( id the carrier of S) by YELLOW_9:def 1;

      then

       A2: (f .: X) = X by FUNCT_1: 92;

      

       A3: ex_sup_of (X,T) by YELLOW_0: 17;

      

       A4: (f . ( sup X)) = ( sup X) by A1;

      ( "\/" (X,T)) in the carrier of S by A3, YELLOW_0:def 19;

      hence thesis by A2, A3, A4, YELLOW_0: 64;

    end;

    theorem :: WAYBEL21:10

    

     Th10: for T be up-complete non empty Poset holds for S be directed-sups-inheriting full non empty SubRelStr of T holds ( incl (S,T)) is directed-sups-preserving

    proof

      let T be up-complete non empty Poset;

      let S be directed-sups-inheriting full non empty SubRelStr of T;

      set f = ( incl (S,T));

      let X be Subset of S;

      assume that

       A1: X is non empty directed and ex_sup_of (X,S);

      reconsider X9 = X as non empty directed Subset of T by A1, YELLOW_2: 7;

      the carrier of S c= the carrier of T by YELLOW_0:def 13;

      then

       A2: f = ( id the carrier of S) by YELLOW_9:def 1;

      then

       A3: (f .: X) = X9 by FUNCT_1: 92;

      

       A4: (f . ( sup X)) = ( sup X) by A2;

      thus ex_sup_of ((f .: X),T) by A3, WAYBEL_0: 75;

      hence thesis by A1, A3, A4, WAYBEL_0: 7;

    end;

    theorem :: WAYBEL21:11

    for T be complete LATTICE holds for S be filtered-infs-inheriting full non empty SubRelStr of T holds ( incl (S,T)) is filtered-infs-preserving

    proof

      let T be complete LATTICE;

      let S be filtered-infs-inheriting full non empty SubRelStr of T;

      set f = ( incl (S,T));

      let X be Subset of S;

      assume that

       A1: X is non empty filtered and ex_inf_of (X,S);

      thus ex_inf_of ((f .: X),T) by YELLOW_0: 17;

      the carrier of S c= the carrier of T by YELLOW_0:def 13;

      then

       A2: f = ( id the carrier of S) by YELLOW_9:def 1;

      then

       A3: (f .: X) = X by FUNCT_1: 92;

      

       A4: ex_inf_of (X,T) by YELLOW_0: 17;

      (f . ( inf X)) = ( inf X) by A2;

      hence thesis by A1, A3, A4, WAYBEL_0: 6;

    end;

    theorem :: WAYBEL21:12

    

     Th12: for T1,T2,R be RelStr, S be SubRelStr of T1 st the RelStr of T1 = the RelStr of T2 & the RelStr of S = the RelStr of R holds R is SubRelStr of T2 & (S is full implies R is full SubRelStr of T2)

    proof

      let T,T2,R be RelStr, S be SubRelStr of T such that

       A1: the RelStr of T = the RelStr of T2 and

       A2: the RelStr of S = the RelStr of R;

      

       A3: the carrier of R c= the carrier of T2 by A1, A2, YELLOW_0:def 13;

      

       A4: the InternalRel of R c= the InternalRel of T2 by A1, A2, YELLOW_0:def 13;

      hence R is SubRelStr of T2 by A3, YELLOW_0:def 13;

      assume the InternalRel of S = (the InternalRel of T |_2 the carrier of S);

      hence thesis by A1, A2, A3, A4, YELLOW_0:def 13, YELLOW_0:def 14;

    end;

    theorem :: WAYBEL21:13

    

     Th13: for T be non empty RelStr holds T is infs-inheriting sups-inheriting full SubRelStr of T

    proof

      let T be non empty RelStr;

      reconsider R = T as full SubRelStr of T by YELLOW_6: 6;

      

       A1: R is infs-inheriting;

      R is sups-inheriting;

      hence thesis by A1;

    end;

    registration

      let T be complete LATTICE;

      cluster complete for CLSubFrame of T;

      existence

      proof

        T is infs-inheriting sups-inheriting full SubRelStr of T by Th13;

        hence thesis;

      end;

    end

    theorem :: WAYBEL21:14

    

     Th14: for T be Semilattice holds for S be full non empty SubRelStr of T holds S is meet-inheriting iff for X be finite non empty Subset of S holds ( "/\" (X,T)) in the carrier of S

    proof

      let T be Semilattice;

      let S be full non empty SubRelStr of T;

      hereby

        assume

         A1: S is meet-inheriting;

        let X be finite non empty Subset of S;

        

         A2: X is finite;

        defpred P[ set] means $1 <> {} implies ( "/\" ($1,T)) in the carrier of S;

        

         A3: P[ {} ];

         A4:

        now

          let y,x be set;

          assume that

           A5: y in X and

           A6: x c= X and

           A7: P[x];

          thus P[(x \/ {y})]

          proof

            assume (x \/ {y}) <> {} ;

            reconsider y9 = y as Element of S by A5;

            reconsider z = y9 as Element of T by YELLOW_0: 58;

            

             A8: x c= the carrier of S by A6, XBOOLE_1: 1;

            the carrier of S c= the carrier of T by YELLOW_0:def 13;

            then

            reconsider x9 = x as finite Subset of T by A6, A8, XBOOLE_1: 1;

            

             A9: ex_inf_of ( {z},T) by YELLOW_0: 38;

            

             A10: ( inf {z}) = y9 by YELLOW_0: 39;

            now

              assume

               A11: x9 <> {} ;

              then ex_inf_of (x9,T) by YELLOW_0: 55;

              then

               A12: ( inf (x9 \/ {z})) = (( inf x9) "/\" z) by A9, A10, YELLOW_2: 4;

               ex_inf_of ( {( inf x9), z},T) by YELLOW_0: 21;

              then ( inf {( inf x9), z}) in the carrier of S by A1, A7, A11;

              hence ( inf (x9 \/ {z})) in the carrier of S by A12, YELLOW_0: 40;

            end;

            hence thesis by A10;

          end;

        end;

         P[X] from FINSET_1:sch 2( A2, A3, A4);

        hence ( "/\" (X,T)) in the carrier of S;

      end;

      assume

       A13: for X be finite non empty Subset of S holds ( "/\" (X,T)) in the carrier of S;

      let x,y be Element of T;

      assume that

       A14: x in the carrier of S and

       A15: y in the carrier of S;

       {x, y} c= the carrier of S by A14, A15, ZFMISC_1: 32;

      hence thesis by A13;

    end;

    theorem :: WAYBEL21:15

    

     Th15: for T be sup-Semilattice holds for S be full non empty SubRelStr of T holds S is join-inheriting iff for X be finite non empty Subset of S holds ( "\/" (X,T)) in the carrier of S

    proof

      let T be sup-Semilattice;

      let S be full non empty SubRelStr of T;

      hereby

        assume

         A1: S is join-inheriting;

        let X be finite non empty Subset of S;

        

         A2: X is finite;

        defpred P[ set] means $1 <> {} implies ( "\/" ($1,T)) in the carrier of S;

        

         A3: P[ {} ];

         A4:

        now

          let y,x be set;

          assume that

           A5: y in X and

           A6: x c= X and

           A7: P[x];

          reconsider y9 = y as Element of S by A5;

          reconsider z = y9 as Element of T by YELLOW_0: 58;

          thus P[(x \/ {y})]

          proof

            assume (x \/ {y}) <> {} ;

            

             A8: x c= the carrier of S by A6, XBOOLE_1: 1;

            the carrier of S c= the carrier of T by YELLOW_0:def 13;

            then

            reconsider x9 = x as finite Subset of T by A6, A8, XBOOLE_1: 1;

            

             A9: ex_sup_of ( {z},T) by YELLOW_0: 38;

            

             A10: ( sup {z}) = y9 by YELLOW_0: 39;

            now

              assume

               A11: x9 <> {} ;

              then ex_sup_of (x9,T) by YELLOW_0: 54;

              then

               A12: ( sup (x9 \/ {z})) = (( sup x9) "\/" z) by A9, A10, YELLOW_2: 3;

               ex_sup_of ( {( sup x9), z},T) by YELLOW_0: 20;

              then ( sup {( sup x9), z}) in the carrier of S by A1, A7, A11;

              hence ( sup (x9 \/ {z})) in the carrier of S by A12, YELLOW_0: 41;

            end;

            hence thesis by A10;

          end;

        end;

         P[X] from FINSET_1:sch 2( A2, A3, A4);

        hence ( "\/" (X,T)) in the carrier of S;

      end;

      assume

       A13: for X be finite non empty Subset of S holds ( "\/" (X,T)) in the carrier of S;

      let x,y be Element of T;

      assume that

       A14: x in the carrier of S and

       A15: y in the carrier of S;

       {x, y} c= the carrier of S by A14, A15, ZFMISC_1: 32;

      hence thesis by A13;

    end;

    theorem :: WAYBEL21:16

    

     Th16: for T be upper-bounded Semilattice holds for S be meet-inheriting full non empty SubRelStr of T st ( Top T) in the carrier of S & S is filtered-infs-inheriting holds S is infs-inheriting

    proof

      let T be upper-bounded Semilattice;

      let S be meet-inheriting full non empty SubRelStr of T such that

       A1: ( Top T) in the carrier of S and

       A2: S is filtered-infs-inheriting;

      let A be Subset of S;

      the carrier of S c= the carrier of T by YELLOW_0:def 13;

      then

      reconsider C = A as Subset of T by XBOOLE_1: 1;

      set F = ( fininfs C);

      assume

       A3: ex_inf_of (A,T);

      then

       A4: ( inf F) = ( inf C) by WAYBEL_0: 60;

      F c= the carrier of S

      proof

        let x be object;

        assume x in F;

        then

        consider Y be finite Subset of C such that

         A5: x = ( "/\" (Y,T)) and ex_inf_of (Y,T);

        reconsider Y as finite Subset of T by XBOOLE_1: 1;

        reconsider Z = Y as finite Subset of S by XBOOLE_1: 1;

        assume

         A6: not x in the carrier of S;

        then Z <> {} by A1, A5;

        hence thesis by A5, A6, Th14;

      end;

      then

      reconsider G = F as non empty Subset of S;

      reconsider G as filtered non empty Subset of S by WAYBEL10: 23;

       A7:

      now

        let Y be finite Subset of C;

        Y c= the carrier of T by XBOOLE_1: 1;

        hence Y <> {} implies ex_inf_of (Y,T) by YELLOW_0: 55;

      end;

       A8:

      now

        let x be Element of T;

        assume x in F;

        then ex Y be finite Subset of C st x = ( "/\" (Y,T)) & ex_inf_of (Y,T);

        hence ex Y be finite Subset of C st ex_inf_of (Y,T) & x = ( "/\" (Y,T));

      end;

      now

        let Y be finite Subset of C;

        reconsider Z = Y as finite Subset of T by XBOOLE_1: 1;

        assume Y <> {} ;

        then ex_inf_of (Z,T) by YELLOW_0: 55;

        hence ( "/\" (Y,T)) in F;

      end;

      then ex_inf_of (G,T) by A3, A7, A8, WAYBEL_0: 58;

      hence thesis by A2, A4;

    end;

    theorem :: WAYBEL21:17

    for T be lower-bounded sup-Semilattice holds for S be join-inheriting full non empty SubRelStr of T st ( Bottom T) in the carrier of S & S is directed-sups-inheriting holds S is sups-inheriting

    proof

      let T be lower-bounded sup-Semilattice;

      let S be join-inheriting full non empty SubRelStr of T such that

       A1: ( Bottom T) in the carrier of S and

       A2: S is directed-sups-inheriting;

      let A be Subset of S;

      the carrier of S c= the carrier of T by YELLOW_0:def 13;

      then

      reconsider C = A as Subset of T by XBOOLE_1: 1;

      set F = ( finsups C);

      assume

       A3: ex_sup_of (A,T);

      then

       A4: ( sup F) = ( sup C) by WAYBEL_0: 55;

      F c= the carrier of S

      proof

        let x be object;

        assume x in F;

        then

        consider Y be finite Subset of C such that

         A5: x = ( "\/" (Y,T)) and ex_sup_of (Y,T);

        reconsider Y as finite Subset of T by XBOOLE_1: 1;

        reconsider Z = Y as finite Subset of S by XBOOLE_1: 1;

        assume

         A6: not x in the carrier of S;

        then Z <> {} by A1, A5;

        hence thesis by A5, A6, Th15;

      end;

      then

      reconsider G = F as non empty Subset of S;

      reconsider G as directed non empty Subset of S by WAYBEL10: 23;

       A7:

      now

        let Y be finite Subset of C;

        Y c= the carrier of T by XBOOLE_1: 1;

        hence Y <> {} implies ex_sup_of (Y,T) by YELLOW_0: 54;

      end;

       A8:

      now

        let x be Element of T;

        assume x in F;

        then ex Y be finite Subset of C st x = ( "\/" (Y,T)) & ex_sup_of (Y,T);

        hence ex Y be finite Subset of C st ex_sup_of (Y,T) & x = ( "\/" (Y,T));

      end;

      now

        let Y be finite Subset of C;

        reconsider Z = Y as finite Subset of T by XBOOLE_1: 1;

        assume Y <> {} ;

        then ex_sup_of (Z,T) by YELLOW_0: 54;

        hence ( "\/" (Y,T)) in F;

      end;

      then ex_sup_of (G,T) by A3, A7, A8, WAYBEL_0: 53;

      hence thesis by A2, A4;

    end;

    theorem :: WAYBEL21:18

    

     Th18: for T be complete LATTICE, S be full non empty SubRelStr of T st S is infs-inheriting holds S is complete

    proof

      let T be complete LATTICE, S be full non empty SubRelStr of T;

      assume

       A1: S is infs-inheriting;

      now

        let X be set;

        set Y = (X /\ the carrier of S);

        reconsider Y as Subset of S by XBOOLE_1: 17;

        

         A2: ex_inf_of (Y,T) by YELLOW_0: 17;

        then ( "/\" (Y,T)) in the carrier of S by A1;

        then ex_inf_of (Y,S) by A2, YELLOW_0: 63;

        hence ex_inf_of (X,S) by YELLOW_0: 50;

      end;

      hence thesis by YELLOW_2: 25;

    end;

    theorem :: WAYBEL21:19

    for T be complete LATTICE, S be full non empty SubRelStr of T st S is sups-inheriting holds S is complete

    proof

      let T be complete LATTICE, S be full non empty SubRelStr of T;

      assume

       A1: S is sups-inheriting;

      now

        let X be set;

        set Y = (X /\ the carrier of S);

        reconsider Y as Subset of S by XBOOLE_1: 17;

        

         A2: ex_sup_of (Y,T) by YELLOW_0: 17;

        then ( "\/" (Y,T)) in the carrier of S by A1;

        then ex_sup_of (Y,S) by A2, YELLOW_0: 64;

        hence ex_sup_of (X,S) by YELLOW_0: 50;

      end;

      hence thesis by YELLOW_2: 24;

    end;

    theorem :: WAYBEL21:20

    for T1,T2 be non empty RelStr holds for S1 be non empty full SubRelStr of T1 holds for S2 be non empty full SubRelStr of T2 st the RelStr of T1 = the RelStr of T2 & the carrier of S1 = the carrier of S2 holds S1 is infs-inheriting implies S2 is infs-inheriting

    proof

      let T1,T2 be non empty RelStr;

      let S1 be non empty full SubRelStr of T1;

      let S2 be non empty full SubRelStr of T2;

      assume

       A1: the RelStr of T1 = the RelStr of T2;

      assume

       A2: the carrier of S1 = the carrier of S2;

      assume

       A3: for X be Subset of S1 st ex_inf_of (X,T1) holds ( "/\" (X,T1)) in the carrier of S1;

      let X be Subset of S2;

      reconsider Y = X as Subset of S1 by A2;

      assume

       A4: ex_inf_of (X,T2);

      then ( "/\" (Y,T1)) in the carrier of S1 by A1, A3, YELLOW_0: 14;

      hence thesis by A1, A2, A4, YELLOW_0: 27;

    end;

    theorem :: WAYBEL21:21

    for T1,T2 be non empty RelStr holds for S1 be non empty full SubRelStr of T1 holds for S2 be non empty full SubRelStr of T2 st the RelStr of T1 = the RelStr of T2 & the carrier of S1 = the carrier of S2 holds S1 is sups-inheriting implies S2 is sups-inheriting

    proof

      let T1,T2 be non empty RelStr;

      let S1 be non empty full SubRelStr of T1;

      let S2 be non empty full SubRelStr of T2;

      assume

       A1: the RelStr of T1 = the RelStr of T2;

      assume

       A2: the carrier of S1 = the carrier of S2;

      assume

       A3: for X be Subset of S1 st ex_sup_of (X,T1) holds ( "\/" (X,T1)) in the carrier of S1;

      let X be Subset of S2;

      reconsider Y = X as Subset of S1 by A2;

      assume

       A4: ex_sup_of (X,T2);

      then ( "\/" (Y,T1)) in the carrier of S1 by A1, A3, YELLOW_0: 14;

      hence thesis by A1, A2, A4, YELLOW_0: 26;

    end;

    theorem :: WAYBEL21:22

    for T1,T2 be non empty RelStr holds for S1 be non empty full SubRelStr of T1 holds for S2 be non empty full SubRelStr of T2 st the RelStr of T1 = the RelStr of T2 & the carrier of S1 = the carrier of S2 holds S1 is directed-sups-inheriting implies S2 is directed-sups-inheriting

    proof

      let T1,T2 be non empty RelStr;

      let S1 be non empty full SubRelStr of T1;

      let S2 be non empty full SubRelStr of T2;

      assume

       A1: the RelStr of T1 = the RelStr of T2;

       the RelStr of S2 = the RelStr of S2;

      then

      reconsider R = S2 as full SubRelStr of T1 by A1, Th12;

      assume

       A2: the carrier of S1 = the carrier of S2;

      then

       A3: the RelStr of S1 = the RelStr of R by YELLOW_0: 57;

      assume

       A4: for X be directed Subset of S1 st X <> {} & ex_sup_of (X,T1) holds ( "\/" (X,T1)) in the carrier of S1;

      let X be directed Subset of S2 such that

       A5: X <> {} ;

      reconsider Y = X as directed Subset of S1 by A3, WAYBEL_0: 3;

      assume

       A6: ex_sup_of (X,T2);

      then ( "\/" (Y,T1)) in the carrier of S1 by A1, A4, A5, YELLOW_0: 14;

      hence thesis by A1, A2, A6, YELLOW_0: 26;

    end;

    theorem :: WAYBEL21:23

    for T1,T2 be non empty RelStr holds for S1 be non empty full SubRelStr of T1 holds for S2 be non empty full SubRelStr of T2 st the RelStr of T1 = the RelStr of T2 & the carrier of S1 = the carrier of S2 holds S1 is filtered-infs-inheriting implies S2 is filtered-infs-inheriting

    proof

      let T1,T2 be non empty RelStr;

      let S1 be non empty full SubRelStr of T1;

      let S2 be non empty full SubRelStr of T2;

      assume

       A1: the RelStr of T1 = the RelStr of T2;

       the RelStr of S2 = the RelStr of S2;

      then

      reconsider R = S2 as full SubRelStr of T1 by A1, Th12;

      assume

       A2: the carrier of S1 = the carrier of S2;

      then

       A3: the RelStr of S1 = the RelStr of R by YELLOW_0: 57;

      assume

       A4: for X be filtered Subset of S1 st X <> {} & ex_inf_of (X,T1) holds ( "/\" (X,T1)) in the carrier of S1;

      let X be filtered Subset of S2 such that

       A5: X <> {} ;

      reconsider Y = X as filtered Subset of S1 by A3, WAYBEL_0: 4;

      assume

       A6: ex_inf_of (X,T2);

      then ( "/\" (Y,T1)) in the carrier of S1 by A1, A4, A5, YELLOW_0: 14;

      hence thesis by A1, A2, A6, YELLOW_0: 27;

    end;

    begin

    theorem :: WAYBEL21:24

    

     Th24: for S,T be non empty TopSpace, N be net of S holds for f be Function of S, T st f is continuous holds (f .: ( Lim N)) c= ( Lim (f * N))

    proof

      let S,T be non empty TopSpace, N be net of S;

      

       A1: ( [#] T) <> {} ;

      let f be Function of S, T such that

       A2: f is continuous;

      let p be object;

      assume

       A3: p in (f .: ( Lim N));

      then

      reconsider p as Point of T;

      consider x be object such that

       A4: x in the carrier of S and

       A5: x in ( Lim N) and

       A6: p = (f . x) by A3, FUNCT_2: 64;

      reconsider x as Element of S by A4;

      now

        let V be a_neighborhood of p;

        

         A7: p in ( Int V) by CONNSP_2:def 1;

        

         A8: x in (f " ( Int V)) by A6, A7, FUNCT_2: 38;

        (f " ( Int V)) is open by A1, A2, TOPS_2: 43;

        then (f " ( Int V)) is a_neighborhood of x by A8, CONNSP_2: 3;

        then N is_eventually_in (f " ( Int V)) by A5, YELLOW_6:def 15;

        then

        consider i be Element of N such that

         A9: for j be Element of N st j >= i holds (N . j) in (f " ( Int V));

        

         A10: the mapping of (f * N) = (f * the mapping of N) by WAYBEL_9:def 8;

        

         A11: the RelStr of (f * N) = the RelStr of N by WAYBEL_9:def 8;

        then

        reconsider i9 = i as Element of (f * N);

        thus (f * N) is_eventually_in V

        proof

          take i9;

          let j9 be Element of (f * N);

          reconsider j = j9 as Element of N by A11;

          

           A12: (f . (N . j)) = ((f * N) . j9) by A10, FUNCT_2: 15;

          assume j9 >= i9;

          then (N . j) in (f " ( Int V)) by A9, A11, YELLOW_0: 1;

          then

           A13: (f . (N . j)) in ( Int V) by FUNCT_2: 38;

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

          hence thesis by A12, A13;

        end;

      end;

      hence thesis by YELLOW_6:def 15;

    end;

    definition

      let T be non empty RelStr;

      let N be non empty NetStr over T;

      :: original: antitone

      redefine

      :: WAYBEL21:def2

      attr N is antitone means

      : Def2: for i,j be Element of N st i <= j holds (N . i) >= (N . j);

      compatibility

      proof

        hereby

          assume N is antitone;

          then

           A1: ( netmap (N,T)) is antitone;

          let i,j be Element of N;

          assume i <= j;

          hence (N . i) >= (N . j) by A1;

        end;

        assume

         A2: for i,j be Element of N st i <= j holds (N . i) >= (N . j);

        let i,j be Element of N;

        

         A3: (N . i) = (( netmap (N,T)) . i);

        (N . j) = (( netmap (N,T)) . j);

        hence thesis by A2, A3;

      end;

    end

    registration

      let T be non empty reflexive RelStr;

      let x be Element of T;

      cluster ( {x} opp+id ) -> transitive directed monotone antitone;

      coherence

      proof

        set N = ( {x} opp+id );

        

         A1: the carrier of N = {x} by YELLOW_9: 7;

        thus N is transitive

        proof

          let i,j,k be Element of N;

          i = x by A1, TARSKI:def 1;

          hence thesis by A1, TARSKI:def 1;

        end;

        thus N is directed

        proof

          let i,j be Element of N;

          

           A2: i = x by A1, TARSKI:def 1;

          

           A3: i <= i;

          j <= i by A1, A2, TARSKI:def 1;

          hence thesis by A3;

        end;

        thus N is monotone

        proof

          let i,j be Element of N;

          

           A4: i = x by A1, TARSKI:def 1;

          j = x by A1, TARSKI:def 1;

          hence thesis by A4, YELLOW_0:def 1;

        end;

        let i,j be Element of N;

        

         A5: i = x by A1, TARSKI:def 1;

        j = x by A1, TARSKI:def 1;

        hence thesis by A5, YELLOW_0:def 1;

      end;

    end

    registration

      let T be non empty reflexive RelStr;

      cluster monotone antitone reflexive strict for net of T;

      existence

      proof

        set x = the Element of T;

        take ( {x} opp+id );

        thus thesis;

      end;

    end

    registration

      let T be non empty RelStr;

      let F be non empty Subset of T;

      cluster (F opp+id ) -> antitone;

      coherence

      proof

        let i,j be Element of (F opp+id );

        

         A1: (F opp+id ) is full SubRelStr of (T opp ) by YELLOW_9: 7;

        then

        reconsider x = i, y = j as Element of (T opp ) by YELLOW_0: 58;

        assume i <= j;

        then x <= y by A1, YELLOW_0: 59;

        then ( ~ x) >= ( ~ y) by YELLOW_7: 1;

        then ((F opp+id ) . i) >= ( ~ y) by YELLOW_9: 7;

        hence thesis by YELLOW_9: 7;

      end;

    end

    registration

      let S,T be non empty reflexive RelStr;

      let f be monotone Function of S, T;

      let N be antitone non empty NetStr over S;

      cluster (f * N) -> antitone;

      coherence

      proof

        let i,j be Element of (f * N);

        

         A1: the mapping of (f * N) = (f * the mapping of N) by WAYBEL_9:def 8;

        

         A2: the RelStr of (f * N) = the RelStr of N by WAYBEL_9:def 8;

        then

        reconsider x = i, y = j as Element of N;

        assume i <= j;

        then x <= y by A2, YELLOW_0: 1;

        then (N . x) >= (N . y) by Def2;

        then (f . (N . x)) >= (f . (N . y)) by WAYBEL_1:def 2;

        then ((f * N) . i) >= (f . (N . y)) by A1, FUNCT_2: 15;

        hence thesis by A1, FUNCT_2: 15;

      end;

    end

    theorem :: WAYBEL21:25

    

     Th25: for S be complete LATTICE, N be net of S holds the set of all ( "/\" ({ (N . i) where i be Element of N : i >= j },S)) where j be Element of N is directed non empty Subset of S

    proof

      let S be complete LATTICE, N be net of S;

      set X = the set of all ( "/\" ({ (N . i) where i be Element of N : i >= j },S)) where j be Element of N;

      X c= the carrier of S

      proof

        let x be object;

        assume x in X;

        then ex j be Element of N st x = ( "/\" ({ (N . i) where i be Element of N : i >= j },S));

        hence thesis;

      end;

      then

      reconsider X as Subset of S;

      X is non empty directed by WAYBEL11: 30;

      hence thesis;

    end;

    theorem :: WAYBEL21:26

    for S be non empty Poset, N be monotone reflexive net of S holds the set of all ( "/\" ({ (N . i) where i be Element of N : i >= j },S)) where j be Element of N is directed non empty Subset of S

    proof

      let S be non empty Poset, N be monotone reflexive net of S;

      set X = the set of all ( "/\" ({ (N . i) where i be Element of N : i >= j },S)) where j be Element of N;

      set jj = the Element of N;

      

       A1: ( "/\" ({ (N . i) where i be Element of N : i >= jj },S)) in X;

      X c= the carrier of S

      proof

        let x be object;

        assume x in X;

        then ex j be Element of N st x = ( "/\" ({ (N . i) where i be Element of N : i >= j },S));

        hence thesis;

      end;

      then

      reconsider X as non empty Subset of S by A1;

      X is directed

      proof

        let x,y be Element of S;

        assume x in X;

        then

        consider j1 be Element of N such that

         A2: x = ( "/\" ({ (N . i) where i be Element of N : i >= j1 },S));

        assume y in X;

        then

        consider j2 be Element of N such that

         A3: y = ( "/\" ({ (N . i) where i be Element of N : i >= j2 },S));

        reconsider j1, j2 as Element of N;

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

        then

        consider j be Element of N such that j in ( [#] N) and

         A4: j >= j1 and

         A5: j >= j2;

        set z = ( "/\" ({ (N . i) where i be Element of N : i >= j },S));

        take z;

        thus z in X;

        deffunc up( Element of N) = { (N . i) where i be Element of N : i >= $1 };

        

         A6: for j be Element of N holds ex_inf_of ( up(j),S)

        proof

          let j be Element of N;

          reconsider j9 = j as Element of N;

          now

            take x = (N . j);

            j9 <= j9;

            then

             A7: x in up(j);

            thus x is_<=_than up(j)

            proof

              let y be Element of S;

              assume y in up(j);

              then ex i be Element of N st y = (N . i) & i >= j;

              hence x <= y by WAYBEL11:def 9;

            end;

            let y be Element of S;

            assume y is_<=_than up(j);

            hence y <= x by A7;

          end;

          hence thesis by YELLOW_0: 16;

        end;

        then

         A8: ex_inf_of ( up(j1),S);

        

         A9: ex_inf_of ( up(j2),S) by A6;

        

         A10: ex_inf_of ( up(j),S) by A6;

        set A = { (N . i) where i be Element of N : i >= j };

        A c= { (N . k) where k be Element of N : k >= j1 }

        proof

          let a be object;

          assume a in A;

          then

          consider k be Element of N such that

           A11: a = (N . k) and

           A12: k >= j;

          reconsider k as Element of N;

          k >= j1 by A4, A12, ORDERS_2: 3;

          hence thesis by A11;

        end;

        hence z >= x by A2, A8, A10, YELLOW_0: 35;

        A c= { (N . k) where k be Element of N : k >= j2 }

        proof

          let a be object;

          assume a in A;

          then

          consider k be Element of N such that

           A13: a = (N . k) and

           A14: k >= j;

          reconsider k as Element of N;

          k >= j2 by A5, A14, ORDERS_2: 3;

          hence thesis by A13;

        end;

        hence thesis by A3, A9, A10, YELLOW_0: 35;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL21:27

    

     Th27: for S be non empty 1-sorted, N be non empty NetStr over S, X be set st ( rng the mapping of N) c= X holds N is_eventually_in X

    proof

      let S be non empty 1-sorted, N be non empty NetStr over S;

      let X be set such that

       A1: ( rng the mapping of N) c= X;

      set i = the Element of N;

      take i;

      let j be Element of N;

      (N . j) in ( rng the mapping of N) by FUNCT_2: 4;

      hence thesis by A1;

    end;

    theorem :: WAYBEL21:28

    

     Th28: for R be /\-complete non empty Poset holds for F be non empty filtered Subset of R holds ( lim_inf (F opp+id )) = ( inf F)

    proof

      let R be /\-complete non empty Poset;

      let F be non empty filtered Subset of R;

      set N = (F opp+id );

      defpred P[ set] means not contradiction;

      deffunc F( Element of N) = ( inf F);

      deffunc G( Element of N) = ( "/\" ({ (N . i) where i be Element of N : i >= $1 },R));

      

       A1: for v be Element of N st P[v] holds F(v) = G(v)

      proof

        let v be Element of N;

        set X = { (N . i) where i be Element of N : i >= v };

        

         A2: the carrier of N = F by YELLOW_9: 7;

        then v in F;

        then

        reconsider j = v as Element of R;

        reconsider vv = v as Element of N;

        

         A3: X c= F

        proof

          let x be object;

          assume x in X;

          then

          consider i be Element of N such that

           A4: x = (N . i) and i >= v;

          reconsider i as Element of N;

          x = i by A4, YELLOW_9: 7;

          hence thesis by A2;

        end;

        vv <= vv;

        then (N . v) in X;

        then

        reconsider X as non empty Subset of R by A3, XBOOLE_1: 1;

        

         A5: ex_inf_of (F,R) by WAYBEL_0: 76;

        

         A6: ex_inf_of (X,R) by WAYBEL_0: 76;

        then

         A7: ( inf X) >= ( inf F) by A3, A5, YELLOW_0: 35;

        F is_>=_than ( inf X)

        proof

          let a be Element of R;

          assume a in F;

          then

          consider b be Element of R such that

           A8: b in F and

           A9: a >= b and

           A10: j >= b by A2, WAYBEL_0:def 2;

          reconsider k = b as Element of N by A8, YELLOW_9: 7;

          

           A11: N is full SubRelStr of (R opp ) by YELLOW_9: 7;

          

           A12: (j ~ ) <= (b ~ ) by A10, LATTICE3: 9;

          

           A13: (N . k) = b by YELLOW_9: 7;

          k >= vv by A11, A12, YELLOW_0: 60;

          then b in X by A13;

          then

           A14: {b} c= X by ZFMISC_1: 31;

          

           A15: ex_inf_of ( {b},R) by YELLOW_0: 38;

          ( inf {b}) = b by YELLOW_0: 39;

          then b >= ( inf X) by A6, A14, A15, YELLOW_0: 35;

          hence thesis by A9, YELLOW_0:def 2;

        end;

        then ( inf F) >= ( "/\" (X,R)) by A5, YELLOW_0: 31;

        hence thesis by A7, ORDERS_2: 2;

      end;

      

       A16: { F(j) where j be Element of N : P[j] } = { G(k) where k be Element of N : P[k] } from FRAENKEL:sch 6( A1);

      

       A17: ex j be Element of N st P[j];

      { ( inf F) where j be Element of N : P[j] } = {( inf F)} from LATTICE3:sch 1( A17);

      

      hence ( lim_inf N) = ( "\/" ( {( inf F)},R)) by A16, WAYBEL11:def 6

      .= ( inf F) by YELLOW_0: 39;

    end;

    theorem :: WAYBEL21:29

    

     Th29: for S,T be /\-complete non empty Poset holds for X be non empty filtered Subset of S holds for f be monotone Function of S, T holds ( lim_inf (f * (X opp+id ))) = ( inf (f .: X))

    proof

      let S,T be /\-complete non empty Poset;

      let X be non empty filtered Subset of S;

      let f be monotone Function of S, T;

      set M = (X opp+id ), N = (f * M);

      deffunc up( Element of N) = { (N . i) where i be Element of N : i >= $1 };

      deffunc infy( Element of N) = ( "/\" ( up($1),T));

      

       A1: the RelStr of N = the RelStr of M by WAYBEL_9:def 8;

      

       A2: the mapping of N = (f * the mapping of M) by WAYBEL_9:def 8;

      

       A3: the carrier of M = X by YELLOW_9: 7;

      

       A4: the mapping of M = ( id X) by WAYBEL19: 27;

      defpred P[ set] means not contradiction;

      deffunc G( set) = ( inf (f .: X));

      

       A5: for j be Element of N st P[j] holds infy(j) = G(j)

      proof

        let j be Element of N;

        reconsider j as Element of N;

        

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

        then

        consider i9 be Element of N such that i9 in ( [#] N) and

         A7: i9 >= j and i9 >= j;

        

         A8: up(j) c= (f .: X)

        proof

          let a be object;

          assume a in up(j);

          then

          consider i be Element of N such that

           A9: a = (N . i) and i >= j;

          reconsider i as Element of N;

          reconsider i9 = i as Element of M by A1;

          

           A10: (N . i) = (f . (( id X) . i)) by A1, A2, A4, FUNCT_2: 15

          .= (f . i9) by A3;

          i9 in X by A3;

          hence thesis by A9, A10, FUNCT_2: 35;

        end;

        then

         A11: up(j) c= the carrier of T by XBOOLE_1: 1;

        (N . i9) in up(j) by A7;

        then

         A12: ex_inf_of ( up(j),T) by A11, WAYBEL_0: 76;

        

         A13: ex_inf_of ((f .: X),T) by WAYBEL_0: 76;

        then

         A14: infy(j) >= ( inf (f .: X)) by A8, A12, YELLOW_0: 35;

         infy(j) is_<=_than (f .: X)

        proof

          let x be Element of T;

          assume x in (f .: X);

          then

          consider y be object such that

           A15: y in the carrier of S and

           A16: y in X and

           A17: x = (f . y) by FUNCT_2: 64;

          reconsider y as Element of N by A1, A16, YELLOW_9: 7;

          consider i be Element of N such that i in ( [#] N) and

           A18: i >= y and

           A19: i >= j by A6;

          i in X by A1, A3;

          then

          reconsider xi = i, xy = y as Element of S by A15;

          M is full SubRelStr of (S opp ) by YELLOW_9: 7;

          then N is full SubRelStr of (S opp ) by A1, Th12;

          then (xi ~ ) >= (xy ~ ) by A18, YELLOW_0: 59;

          then xi <= xy by LATTICE3: 9;

          then

           A20: (f . xi) <= x by A17, WAYBEL_1:def 2;

          (N . i) = (f . (( id X) . i)) by A1, A2, A4, FUNCT_2: 15

          .= (f . xi) by A1, A3;

          then (f . xi) in up(j) by A19;

          then (f . xi) >= infy(j) by A12, YELLOW_4: 2;

          hence thesis by A20, ORDERS_2: 3;

        end;

        then infy(j) <= ( inf (f .: X)) by A13, YELLOW_0: 31;

        hence thesis by A14, ORDERS_2: 2;

      end;

      

       A21: ex j be Element of N st P[j];

      { infy(j) where j be Element of N : P[j] } = { G(j) where j be Element of N : P[j] } from FRAENKEL:sch 6( A5)

      .= { ( inf (f .: X)) where j be Element of N : P[j] }

      .= {( inf (f .: X))} from LATTICE3:sch 1( A21);

      

      hence ( lim_inf N) = ( sup {( inf (f .: X))}) by WAYBEL11:def 6

      .= ( inf (f .: X)) by YELLOW_0: 39;

    end;

    theorem :: WAYBEL21:30

    

     Th30: for S,T be non empty TopPoset holds for X be non empty filtered Subset of S holds for f be monotone Function of S, T holds for Y be non empty filtered Subset of T st Y = (f .: X) holds (f * (X opp+id )) is subnet of (Y opp+id )

    proof

      let S,T be non empty TopPoset;

      let X be non empty filtered Subset of S;

      let f be monotone Function of S, T;

      let Y be non empty filtered Subset of T such that

       A1: Y = (f .: X);

      set N = (f * (X opp+id )), M = (Y opp+id );

      

       A2: the RelStr of N = the RelStr of (X opp+id ) by WAYBEL_9:def 8;

      

       A3: the mapping of N = (f * the mapping of (X opp+id )) by WAYBEL_9:def 8;

      

       A4: the carrier of M = Y by YELLOW_9: 7;

      

       A5: the mapping of M = ( id Y) by WAYBEL19: 27;

      

       A6: the carrier of (X opp+id ) = X by YELLOW_9: 7;

      the mapping of (X opp+id ) = ( id X) by WAYBEL19: 27;

      then

       A7: the mapping of N = (f | X) by A3, RELAT_1: 65;

      then

       A8: ( rng the mapping of N) = (f .: X) by RELAT_1: 115;

      ( dom the mapping of N) = X by A2, A6, FUNCT_2:def 1;

      then

      reconsider g = (f | X) as Function of N, M by A1, A2, A4, A6, A7, A8, FUNCT_2:def 1, RELSET_1: 4;

      take g;

      thus the mapping of N = (the mapping of M * g) by A1, A5, A7, A8, RELAT_1: 53;

      let m be Element of M;

      consider n be object such that

       A9: n in the carrier of S and

       A10: n in X and

       A11: m = (f . n) by A1, A4, FUNCT_2: 64;

      reconsider n as Element of N by A2, A10, YELLOW_9: 7;

      take n;

      let p be Element of N;

      p in X by A2, A6;

      then

      reconsider n9 = n, p9 = p as Element of S by A9;

      reconsider fp = (f . p9) as Element of M by A1, A2, A4, A6, FUNCT_2: 35;

      (X opp+id ) is SubRelStr of (S opp ) by YELLOW_9: 7;

      then

       A12: N is SubRelStr of (S opp ) by A2, Th12;

      

       A13: M is full SubRelStr of (T opp ) by YELLOW_9: 7;

      assume n <= p;

      then (n9 ~ ) <= (p9 ~ ) by A12, YELLOW_0: 59;

      then n9 >= p9 by LATTICE3: 9;

      then (f . n9) >= (f . p9) by WAYBEL_1:def 2;

      then ((f . n9) ~ ) <= ((f . p9) ~ ) by LATTICE3: 9;

      then fp >= m by A11, A13, YELLOW_0: 60;

      hence m <= (g . p) by A2, A6, FUNCT_1: 49;

    end;

    theorem :: WAYBEL21:31

    for S,T be non empty TopPoset holds for X be non empty filtered Subset of S holds for f be monotone Function of S, T holds for Y be non empty filtered Subset of T st Y = (f .: X) holds ( Lim (Y opp+id )) c= ( Lim (f * (X opp+id )))

    proof

      let S,T be non empty TopPoset;

      let X be non empty filtered Subset of S;

      let f be monotone Function of S, T;

      let Y be non empty filtered Subset of T;

      assume Y = (f .: X);

      then (f * (X opp+id )) is subnet of (Y opp+id ) by Th30;

      hence thesis by YELLOW_6: 32;

    end;

    theorem :: WAYBEL21:32

    

     Th32: for S be non empty reflexive RelStr, D be non empty Subset of S holds the mapping of ( Net-Str D) = ( id D) & the carrier of ( Net-Str D) = D & ( Net-Str D) is full SubRelStr of S

    proof

      let S be non empty reflexive RelStr, D be non empty Subset of S;

      set N = ( Net-Str D);

      

       A1: ( dom ( id D)) = D;

      ( rng ( id D)) = D;

      then

      reconsider g = ( id D) as Function of D, the carrier of S by A1, FUNCT_2:def 1, RELSET_1: 4;

      (( id the carrier of S) | D) = ( id D) by FUNCT_3: 1;

      then

       A2: N = NetStr (# D, (the InternalRel of S |_2 D), g #) by WAYBEL17:def 4;

      then the InternalRel of N c= the InternalRel of S by XBOOLE_1: 17;

      hence thesis by A2, YELLOW_0:def 13, YELLOW_0:def 14;

    end;

    theorem :: WAYBEL21:33

    

     Th33: for S,T be up-complete non empty Poset holds for f be monotone Function of S, T holds for D be non empty directed Subset of S holds ( lim_inf (f * ( Net-Str D))) = ( sup (f .: D))

    proof

      let S,T be up-complete non empty Poset, f be monotone Function of S, T;

      let X be non empty directed Subset of S;

      set M = ( Net-Str X), N = (f * M);

      deffunc up( Element of N) = { (N . i) where i be Element of N : i >= $1 };

      deffunc infy( Element of N) = ( "/\" ( up($1),T));

      set NT = the set of all infy(j) where j be Element of N;

      

       A1: the RelStr of N = the RelStr of M by WAYBEL_9:def 8;

      

       A2: the mapping of N = (f * the mapping of M) by WAYBEL_9:def 8;

      

       A3: the carrier of M = X by Th32;

      

       A4: the mapping of M = ( id X) by Th32;

       A5:

      now

        let i be Element of N;

        

        thus (N . i) = (f . (( id X) . i)) by A1, A2, A4, FUNCT_2: 15

        .= (f . i) by A1, A3;

      end;

      

       A6: for i be Element of N holds infy(i) = (f . i)

      proof

        let i be Element of N;

        i in X by A1, A3;

        then

        reconsider x = i as Element of S;

        

         A7: i <= i;

        (N . i) = (f . x) by A5;

        then (f . x) in up(i) by A7;

        then

         A8: for z be Element of T st z is_<=_than up(i) holds z <= (f . x);

        (f . x) is_<=_than up(i)

        proof

          let z be Element of T;

          assume z in up(i);

          then

          consider j be Element of N such that

           A9: z = (N . j) and

           A10: j >= i;

          reconsider j as Element of N;

          j in X by A1, A3;

          then

          reconsider y = j as Element of S;

          

           A11: M is full SubRelStr of S by Th32;

           the RelStr of S = the RelStr of S;

          then N is full SubRelStr of S by A1, A11, Th12;

          then y >= x by A10, YELLOW_0: 59;

          then (f . y) >= (f . x) by WAYBEL_1:def 2;

          hence thesis by A5, A9;

        end;

        hence thesis by A8, YELLOW_0: 31;

      end;

      NT = (f .: X)

      proof

        thus NT c= (f .: X)

        proof

          let x be object;

          assume x in NT;

          then

          consider j be Element of N such that

           A12: x = infy(j);

          reconsider j as Element of N;

          

           A13: x = (f . j) by A6, A12;

          j in X by A1, A3;

          hence thesis by A13, FUNCT_2: 35;

        end;

        let y be object;

        assume y in (f .: X);

        then

        consider x be object such that

         A14: x in the carrier of S and

         A15: x in X and

         A16: y = (f . x) by FUNCT_2: 64;

        reconsider x as Element of S by A14;

        reconsider i = x as Element of N by A1, A15, Th32;

        (f . x) = infy(i) by A6;

        hence thesis by A16;

      end;

      hence thesis by WAYBEL11:def 6;

    end;

    theorem :: WAYBEL21:34

    

     Th34: for S be non empty reflexive RelStr holds for D be non empty directed Subset of S holds for i,j be Element of ( Net-Str D) holds i <= j iff (( Net-Str D) . i) <= (( Net-Str D) . j)

    proof

      let S be non empty reflexive RelStr;

      let D be non empty directed Subset of S;

      

       A1: ( dom ( id D)) = D;

      ( rng ( id D)) = D;

      then

      reconsider g = ( id D) as Function of D, the carrier of S by A1, FUNCT_2:def 1, RELSET_1: 4;

      (( id the carrier of S) | D) = ( id D) by FUNCT_3: 1;

      then ( Net-Str D) = ( Net-Str (D,g)) by WAYBEL17: 9;

      hence thesis by WAYBEL11:def 10;

    end;

    theorem :: WAYBEL21:35

    

     Th35: for T be Lawson complete TopLattice holds for D be directed non empty Subset of T holds ( sup D) in ( Lim ( Net-Str D))

    proof

      let T be Lawson complete TopLattice;

      let D be directed non empty Subset of T;

      set N = ( Net-Str D);

      

       A1: the mapping of N = ( id D) by Th32;

      

       A2: the carrier of N = D by Th32;

      set K = the prebasis of T;

      now

        let A be Subset of T;

        assume

         A3: ( sup D) in A;

        

         A4: K c= the topology of T by TOPS_2: 64;

        assume A in K;

        then A is open by A4, PRE_TOPC:def 2;

        then A is property(S) by WAYBEL19: 36;

        then

        consider y be Element of T such that

         A5: y in D and

         A6: for x be Element of T st x in D & x >= y holds x in A by A3, WAYBEL11:def 3;

        reconsider i = y as Element of N by A5, Th32;

        thus N is_eventually_in A

        proof

          take i;

          let j be Element of N;

          

           A7: j = (N . j) by A1, A2;

          

           A8: y = (N . i) by A1, A2;

          assume j >= i;

          then (N . j) >= (N . i) by Th34;

          hence thesis by A2, A6, A7, A8;

        end;

      end;

      hence thesis by WAYBEL19: 25;

    end;

    definition

      let T be non empty 1-sorted;

      let N be net of T, M be non empty NetStr over T;

      :: WAYBEL21:def3

      mode Embedding of M,N -> Function of M, N means

      : Def3: the mapping of M = (the mapping of N * it ) & for m be Element of N holds ex n be Element of M st for p be Element of M st n <= p holds m <= (it . p);

      existence by A1, YELLOW_6:def 9;

    end

    theorem :: WAYBEL21:36

    

     Th36: for T be non empty 1-sorted holds for N be net of T, M be subnet of N holds for e be Embedding of M, N, i be Element of M holds (M . i) = (N . (e . i))

    proof

      let T be non empty 1-sorted;

      let N be net of T, M be subnet of N;

      let e be Embedding of M, N, i be Element of M;

      the mapping of M = (the mapping of N * e) by Def3;

      hence thesis by FUNCT_2: 15;

    end;

    theorem :: WAYBEL21:37

    

     Th37: for T be complete LATTICE holds for N be net of T, M be subnet of N holds ( lim_inf N) <= ( lim_inf M)

    proof

      let T be complete LATTICE;

      let N be net of T, M be subnet of N;

      deffunc infy( net of T) = the set of all ( "/\" ({ ($1 . i) where i be Element of $1 : i >= j },T)) where j be Element of $1;

      

       A1: ( "\/" ( infy(M),T)) is_>=_than infy(N)

      proof

        let t be Element of T;

        assume t in infy(N);

        then

        consider j be Element of N such that

         A2: t = ( "/\" ({ (N . i) where i be Element of N : i >= j },T));

        set e = the Embedding of M, N;

        reconsider j as Element of N;

        consider j9 be Element of M such that

         A3: for p be Element of M st j9 <= p holds j <= (e . p) by Def3;

        set X = { (N . i) where i be Element of N : i >= j };

        set Y = { (M . i) where i be Element of M : i >= j9 };

        

         A4: ex_inf_of (X,T) by YELLOW_0: 17;

        

         A5: ex_inf_of (Y,T) by YELLOW_0: 17;

        Y c= X

        proof

          let y be object;

          assume y in Y;

          then

          consider i be Element of M such that

           A6: y = (M . i) and

           A7: i >= j9;

          reconsider i as Element of M;

          (e . i) >= j by A3, A7;

          then (N . (e . i)) in X;

          hence thesis by A6, Th36;

        end;

        then

         A8: t <= ( "/\" (Y,T)) by A2, A4, A5, YELLOW_0: 35;

        ( "/\" (Y,T)) in infy(M);

        then ( "/\" (Y,T)) <= ( "\/" ( infy(M),T)) by YELLOW_2: 22;

        hence thesis by A8, YELLOW_0:def 2;

      end;

      

       A9: ( lim_inf M) = ( "\/" ( infy(M),T)) by WAYBEL11:def 6;

      ( lim_inf N) = ( "\/" ( infy(N),T)) by WAYBEL11:def 6;

      hence thesis by A1, A9, YELLOW_0: 32;

    end;

    theorem :: WAYBEL21:38

    

     Th38: for T be complete LATTICE holds for N be net of T, M be subnet of N holds for e be Embedding of M, N st for i be Element of N, j be Element of M st (e . j) <= i holds ex j9 be Element of M st j9 >= j & (N . i) >= (M . j9) holds ( lim_inf N) = ( lim_inf M)

    proof

      let T be complete LATTICE;

      let N be net of T, M be subnet of N;

      let e be Embedding of M, N such that

       A1: for i be Element of N, j be Element of M st (e . j) <= i holds ex j9 be Element of M st j9 >= j & (N . i) >= (M . j9);

      deffunc infy( net of T) = the set of all ( "/\" ({ ($1 . i) where i be Element of $1 : i >= j },T)) where j be Element of $1;

      ( "\/" ( infy(N),T)) is_>=_than infy(M)

      proof

        let t be Element of T;

        assume t in infy(M);

        then

        consider j be Element of M such that

         A2: t = ( "/\" ({ (M . i) where i be Element of M : i >= j },T));

        reconsider j as Element of M;

        set j9 = (e . j);

        set X = { (N . i) where i be Element of N : i >= j9 };

        set Y = { (M . i) where i be Element of M : i >= j };

        t is_<=_than X

        proof

          let x be Element of T;

          assume x in X;

          then

          consider i be Element of N such that

           A3: x = (N . i) and

           A4: i >= j9;

          reconsider i as Element of N;

          consider k be Element of M such that

           A5: k >= j and

           A6: (N . i) >= (M . k) by A1, A4;

          (M . k) in Y by A5;

          then (M . k) >= t by A2, YELLOW_2: 22;

          hence thesis by A3, A6, YELLOW_0:def 2;

        end;

        then

         A7: t <= ( "/\" (X,T)) by YELLOW_0: 33;

        ( "/\" (X,T)) in infy(N);

        then ( "/\" (X,T)) <= ( "\/" ( infy(N),T)) by YELLOW_2: 22;

        hence t <= ( "\/" ( infy(N),T)) by A7, YELLOW_0:def 2;

      end;

      then ( "\/" ( infy(N),T)) >= ( "\/" ( infy(M),T)) by YELLOW_0: 32;

      then ( lim_inf N) >= ( "\/" ( infy(M),T)) by WAYBEL11:def 6;

      then

       A8: ( lim_inf N) >= ( lim_inf M) by WAYBEL11:def 6;

      ( lim_inf M) >= ( lim_inf N) by Th37;

      hence thesis by A8, YELLOW_0:def 3;

    end;

    theorem :: WAYBEL21:39

    for T be non empty RelStr holds for N be net of T, M be non empty full SubNetStr of N st for i be Element of N holds ex j be Element of N st j >= i & j in the carrier of M holds M is subnet of N & ( incl (M,N)) is Embedding of M, N

    proof

      let T be non empty RelStr;

      let N be net of T, M be non empty full SubNetStr of N such that

       A1: for i be Element of N holds ex j be Element of N st j >= i & j in the carrier of M;

      

       A2: the mapping of M = (the mapping of N | the carrier of M) by YELLOW_6:def 6;

      

       A3: M is full SubRelStr of N by YELLOW_6:def 7;

      then

       A4: the carrier of M c= the carrier of N by YELLOW_0:def 13;

      M is directed

      proof

        let x,y be Element of M;

        reconsider i = x, j = y as Element of N by A3, YELLOW_0: 58;

        consider k be Element of N such that

         A5: k >= i and

         A6: k >= j by YELLOW_6:def 3;

        consider l be Element of N such that

         A7: l >= k and

         A8: l in the carrier of M by A1;

        reconsider z = l as Element of M by A8;

        take z;

        

         A9: l >= i by A5, A7, YELLOW_0:def 2;

        l >= j by A6, A7, YELLOW_0:def 2;

        hence thesis by A9, YELLOW_6: 12;

      end;

      then

      reconsider K = M as net of T by A3;

       A10:

      now

        set f = ( incl (K,N));

        

         A11: f = ( id the carrier of K) by A4, YELLOW_9:def 1;

        hence the mapping of K = (the mapping of N * f) by A2, RELAT_1: 65;

        let m be Element of N;

        consider j be Element of N such that

         A12: j >= m and

         A13: j in the carrier of K by A1;

        reconsider n = j as Element of K by A13;

        take n;

        let p be Element of K;

        reconsider q = p as Element of N by A3, YELLOW_0: 58;

        assume n <= p;

        then

         A14: j <= q by YELLOW_6: 11;

        (f . p) = q by A11;

        hence m <= (f . p) by A12, A14, YELLOW_0:def 2;

      end;

      hence M is subnet of N by YELLOW_6:def 9;

      hence thesis by A10, Def3;

    end;

    theorem :: WAYBEL21:40

    

     Th40: for T be non empty RelStr, N be net of T holds for i be Element of N holds (N | i) is subnet of N & ( incl ((N | i),N)) is Embedding of (N | i), N

    proof

      let T be non empty RelStr, N be net of T;

      let i be Element of N;

      set M = (N | i), f = ( incl (M,N));

      thus (N | i) is subnet of N;

      thus (N | i) is subnet of N;

      (N | i) is full SubNetStr of N by WAYBEL_9: 14;

      then

       A1: (N | i) is full SubRelStr of N by YELLOW_6:def 7;

      

       A2: ( incl ((N | i),N)) = ( id the carrier of (N | i)) by WAYBEL_9: 13, YELLOW_9:def 1;

      the mapping of M = (the mapping of N | the carrier of M) by WAYBEL_9:def 7;

      hence the mapping of M = (the mapping of N * f) by A2, RELAT_1: 65;

      let m be Element of N;

      consider n9 be Element of N such that

       A3: n9 >= i and

       A4: n9 >= m by YELLOW_6:def 3;

      reconsider n = n9 as Element of M by A3, WAYBEL_9:def 7;

      take n;

      let p be Element of M;

      reconsider p9 = p as Element of N by A1, YELLOW_0: 58;

      assume n <= p;

      then n9 <= p9 by A1, YELLOW_0: 59;

      then m <= p9 by A4, YELLOW_0:def 2;

      hence thesis by A2;

    end;

    theorem :: WAYBEL21:41

    

     Th41: for T be complete LATTICE, N be net of T holds for i be Element of N holds ( lim_inf (N | i)) = ( lim_inf N)

    proof

      let T be complete LATTICE, N be net of T;

      let i be Element of N;

      reconsider M = (N | i) as subnet of N;

      reconsider e = ( incl (M,N)) as Embedding of M, N by Th40;

      M is full SubNetStr of N by WAYBEL_9: 14;

      then

       A1: M is full SubRelStr of N by YELLOW_6:def 7;

      

       A2: ( incl (M,N)) = ( id the carrier of M) by WAYBEL_9: 13, YELLOW_9:def 1;

      now

        let k be Element of N, j be Element of M;

        consider j9 be Element of N such that

         A3: j9 = j and

         A4: j9 >= i by WAYBEL_9:def 7;

        assume (e . j) <= k;

        then

         A5: k >= j9 by A2, A3;

        then k >= i by A4, YELLOW_0:def 2;

        then

        reconsider k9 = k as Element of M by WAYBEL_9:def 7;

        take k9;

        thus k9 >= j by A1, A3, A5, YELLOW_0: 60;

        

         A6: (M . k9) = (N . (e . k9)) by Th36;

        (M . k9) <= (M . k9);

        hence (N . k) >= (M . k9) by A2, A6;

      end;

      hence thesis by Th38;

    end;

    theorem :: WAYBEL21:42

    

     Th42: for T be non empty RelStr, N be net of T, X be set st N is_eventually_in X holds ex i be Element of N st (N . i) in X & ( rng the mapping of (N | i)) c= X

    proof

      let T be non empty RelStr, N be net of T, X be set;

      given i9 be Element of N such that

       A1: for j be Element of N st j >= i9 holds (N . j) in X;

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

      then

      consider i be Element of N such that i in ( [#] N) and

       A2: i9 <= i and i9 <= i;

      take i;

      thus (N . i) in X by A1, A2;

      let x be object;

      assume x in ( rng the mapping of (N | i));

      then

      consider j be object such that

       A3: j in ( dom the mapping of (N | i)) and

       A4: x = (the mapping of (N | i) . j) by FUNCT_1:def 3;

      

       A5: ( dom the mapping of (N | i)) = the carrier of (N | i) by FUNCT_2:def 1;

      reconsider j as Element of (N | i) by A3;

      the carrier of (N | i) = { y where y be Element of N : i <= y } by WAYBEL_9: 12;

      then

      consider k be Element of N such that

       A6: j = k and

       A7: i <= k by A3, A5;

      x = ((N | i) . j) by A4

      .= (N . k) by A6, WAYBEL_9: 16;

      hence thesis by A1, A2, A7, ORDERS_2: 3;

    end;

    theorem :: WAYBEL21:43

    

     Th43: for T be Lawson complete TopLattice holds for N be eventually-filtered net of T holds ( rng the mapping of N) is filtered non empty Subset of T

    proof

      let T be Lawson complete TopLattice;

      let N be eventually-filtered net of T;

      reconsider F = ( rng the mapping of N) as non empty Subset of T;

      F is filtered

      proof

        let x,y be Element of T;

        assume x in F;

        then

        consider i1 be object such that

         A1: i1 in ( dom the mapping of N) and

         A2: x = (the mapping of N . i1) by FUNCT_1:def 3;

        assume y in F;

        then

        consider i2 be object such that

         A3: i2 in ( dom the mapping of N) and

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

        

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

        reconsider i1, i2 as Element of N by A1, A3;

        consider j1 be Element of N such that

         A6: for k be Element of N st j1 <= k holds (N . i1) >= (N . k) by WAYBEL_0: 12;

        consider j2 be Element of N such that

         A7: for k be Element of N st j2 <= k holds (N . i2) >= (N . k) by WAYBEL_0: 12;

        consider j be Element of N such that

         A8: j2 <= j and

         A9: j1 <= j by YELLOW_6:def 3;

        take z = (N . j);

        thus z in F by A5, FUNCT_1:def 3;

        thus thesis by A2, A4, A6, A7, A8, A9;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL21:44

    

     Th44: for T be Lawson complete TopLattice holds for N be eventually-filtered net of T holds ( Lim N) = {( inf N)}

    proof

      let T be Lawson complete TopLattice;

      set S = the Scott TopAugmentation of T;

      let N be eventually-filtered net of T;

      reconsider F = ( rng the mapping of N) as filtered non empty Subset of T by Th43;

      

       A1: the topology of S = ( sigma T) by YELLOW_9: 51;

      

       A2: the RelStr of S = the RelStr of T by YELLOW_9:def 4;

      

       A3: ( inf N) = ( Inf the mapping of N) by WAYBEL_9:def 2

      .= ( "/\" (F,T)) by YELLOW_2:def 6;

      

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

      thus ( Lim N) c= {( inf N)}

      proof

        let p be object;

        assume

         A5: p in ( Lim N);

        then

        reconsider p as Element of T;

        p is_<=_than F

        proof

          let u be Element of T;

          assume u in F;

          then

          consider i be object such that

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

           A7: u = (the mapping of N . i) by FUNCT_1:def 3;

          reconsider i as Element of N by A6;

          consider ii be Element of N such that

           A8: for k be Element of N st ii <= k holds (N . i) >= (N . k) by WAYBEL_0: 12;

          ( downarrow u) is closed by WAYBEL19: 38;

          then

           A9: ( Cl ( downarrow u)) = ( downarrow u) by PRE_TOPC: 22;

          N is_eventually_in ( downarrow u)

          proof

            take ii;

            let j be Element of N;

            assume j >= ii;

            then (N . j) <= (N . i) by A8;

            hence thesis by A7, WAYBEL_0: 17;

          end;

          then ( Lim N) c= ( downarrow u) by A9, WAYBEL19: 26;

          hence thesis by A5, WAYBEL_0: 17;

        end;

        then

         A10: p <= ( inf N) by A3, YELLOW_0: 33;

        ( inf N) is_<=_than F by A3, YELLOW_0: 33;

        then

         A11: F c= ( uparrow ( inf N)) by YELLOW_2: 2;

        ( uparrow ( inf N)) is closed by WAYBEL19: 38;

        then ( Cl ( uparrow ( inf N))) = ( uparrow ( inf N)) by PRE_TOPC: 22;

        then

         A12: ( Cl F) c= ( uparrow ( inf N)) by A11, PRE_TOPC: 19;

        p in ( Cl F) by A5, WAYBEL_9: 24;

        then p >= ( inf N) by A12, WAYBEL_0: 18;

        then p = ( inf N) by A10, ORDERS_2: 2;

        hence thesis by TARSKI:def 1;

      end;

      reconsider K = (( sigma T) \/ the set of all (( uparrow x) ` ) where x be Element of T) as prebasis of T by WAYBEL19: 30;

      now

        let A be Subset of T;

        assume that

         A13: ( inf F) in A and

         A14: A in K;

        per cases by A14, XBOOLE_0:def 3;

          suppose

           A15: A in ( sigma T);

          then

          reconsider a = A as Subset of S by A1;

          a is open by A1, A15, PRE_TOPC:def 2;

          then a is upper by WAYBEL11:def 4;

          then

           A16: A is upper by A2, WAYBEL_0: 25;

          set i = the Element of N;

          thus N is_eventually_in A

          proof

            take i;

            let j be Element of N;

            (N . j) in F by A4, FUNCT_1:def 3;

            then (N . j) >= ( inf F) by YELLOW_2: 22;

            hence thesis by A13, A16;

          end;

        end;

          suppose A in the set of all (( uparrow x) ` ) where x be Element of T;

          then

          consider x be Element of T such that

           A17: A = (( uparrow x) ` );

           not ( inf F) >= x by A13, A17, YELLOW_9: 1;

          then not F is_>=_than x by YELLOW_0: 33;

          then

          consider y be Element of T such that

           A18: y in F and

           A19: not y >= x;

          consider i be object such that

           A20: i in the carrier of N and

           A21: y = (the mapping of N . i) by A4, A18, FUNCT_1:def 3;

          thus N is_eventually_in A

          proof

            reconsider i as Element of N by A20;

            consider ii be Element of N such that

             A22: for k be Element of N st ii <= k holds (N . i) >= (N . k) by WAYBEL_0: 12;

            take ii;

            let j be Element of N;

            assume j >= ii;

            then (N . j) <= (N . i) by A22;

            then not (N . j) >= x by A19, A21, ORDERS_2: 3;

            hence thesis by A17, YELLOW_9: 1;

          end;

        end;

      end;

      then ( inf F) in ( Lim N) by WAYBEL19: 25;

      hence thesis by A3, ZFMISC_1: 31;

    end;

    begin

    theorem :: WAYBEL21:45

    

     Th45: for S,T be Lawson complete TopLattice holds for f be meet-preserving Function of S, T holds f is continuous iff f is directed-sups-preserving & for X be non empty Subset of S holds f preserves_inf_of X

    proof

      let S,T be Lawson complete TopLattice;

      

       A1: ( [#] T) <> {} ;

      set Ss = the Scott TopAugmentation of S, Ts = the Scott TopAugmentation of T, Sl = the lower correct TopAugmentation of S, Tl = the lower correct TopAugmentation of T;

      

       A2: S is TopAugmentation of S by YELLOW_9: 44;

      

       A3: T is TopAugmentation of T by YELLOW_9: 44;

      

       A4: S is Refinement of Ss, Sl by A2, WAYBEL19: 29;

      

       A5: T is Refinement of Ts, Tl by A3, WAYBEL19: 29;

      

       A6: T is TopAugmentation of Ts by YELLOW_9: 45;

      

       A7: S is TopAugmentation of Ss by YELLOW_9: 45;

      

       A8: the RelStr of Ss = the RelStr of S by YELLOW_9:def 4;

      

       A9: the RelStr of Sl = the RelStr of S by YELLOW_9:def 4;

      

       A10: the RelStr of Ts = the RelStr of T by YELLOW_9:def 4;

      

       A11: the RelStr of Tl = the RelStr of T by YELLOW_9:def 4;

      let f be meet-preserving Function of S, T;

      reconsider g = f as Function of Sl, Tl by A9, A11;

      reconsider h = f as Function of Ss, Ts by A8, A10;

      

       A12: ( [#] Ts) <> {} ;

      hereby

        assume

         A13: f is continuous;

        now

          let P be Subset of Ts;

          reconsider A = P as Subset of Ts;

          reconsider C = A as Subset of T by A10;

          assume

           A14: P is open;

          then C is open by A6, WAYBEL19: 37;

          then

           A15: (f " C) is open by A1, A13, TOPS_2: 43;

          A is upper by A14, WAYBEL11:def 4;

          then (h " A) is upper by A8, A10, WAYBEL17: 2, WAYBEL_9: 1;

          then (f " C) is upper by A8, WAYBEL_0: 25;

          hence (h " P) is open by A7, A15, WAYBEL19: 41;

        end;

        then h is continuous by A12, TOPS_2: 43;

        hence f is directed-sups-preserving by A8, A10, Th6;

        for X be non empty filtered Subset of S holds f preserves_inf_of X

        proof

          let F be non empty filtered Subset of S;

          assume ex_inf_of (F,S);

          thus ex_inf_of ((f .: F),T) by YELLOW_0: 17;

           {( inf F)} = ( Lim (F opp+id )) by WAYBEL19: 43;

          then ( Im (f,( inf F))) c= ( Lim (f * (F opp+id ))) by A13, Th24;

          then {(f . ( inf F))} c= ( Lim (f * (F opp+id ))) by SETWISEO: 8;

          then

           A16: (f . ( inf F)) in ( Lim (f * (F opp+id ))) by ZFMISC_1: 31;

          reconsider G = (f .: F) as filtered non empty Subset of T by WAYBEL20: 24;

          

           A17: ( rng the mapping of (f * (F opp+id ))) = ( rng (f * the mapping of (F opp+id ))) by WAYBEL_9:def 8

          .= ( rng (f * ( id F))) by WAYBEL19: 27

          .= ( rng (f | F)) by RELAT_1: 65

          .= G by RELAT_1: 115;

          ( Lim (f * (F opp+id ))) = {( inf (f * (F opp+id )))} by Th44

          .= {( Inf the mapping of (f * (F opp+id )))} by WAYBEL_9:def 2

          .= {( inf G)} by A17, YELLOW_2:def 6;

          hence thesis by A16, TARSKI:def 1;

        end;

        hence for X be non empty Subset of S holds f preserves_inf_of X by Th4;

      end;

      assume f is directed-sups-preserving;

      then

       A18: h is directed-sups-preserving by A8, A10, Th6;

      assume for X be non empty Subset of S holds f preserves_inf_of X;

      then for X be non empty Subset of Sl holds g preserves_inf_of X by A9, A11, WAYBEL_0: 65;

      then g is continuous by WAYBEL19: 8;

      hence thesis by A4, A5, A18, WAYBEL19: 24;

    end;

    theorem :: WAYBEL21:46

    

     Th46: for S,T be Lawson complete TopLattice holds for f be SemilatticeHomomorphism of S, T holds f is continuous iff f is infs-preserving directed-sups-preserving

    proof

      let S,T be Lawson complete TopLattice;

      let f be SemilatticeHomomorphism of S, T;

      hereby

        assume

         A1: f is continuous;

        

         A2: for X be finite Subset of S holds f preserves_inf_of X by Def1;

        for X be non empty filtered Subset of S holds f preserves_inf_of X by A1, Th45;

        hence f is infs-preserving by A2, WAYBEL_0: 71;

        thus f is directed-sups-preserving by A1, Th45;

      end;

      assume f is infs-preserving;

      then for X be non empty Subset of S holds f preserves_inf_of X;

      hence thesis by Th45;

    end;

    definition

      let S,T be non empty RelStr;

      let f be Function of S, T;

      :: WAYBEL21:def4

      attr f is lim_infs-preserving means for N be net of S holds (f . ( lim_inf N)) = ( lim_inf (f * N));

    end

    theorem :: WAYBEL21:47

    for S,T be Lawson complete TopLattice holds for f be SemilatticeHomomorphism of S, T holds f is continuous iff f is lim_infs-preserving

    proof

      let S,T be Lawson complete TopLattice;

      let f be SemilatticeHomomorphism of S, T;

      thus f is continuous implies f is lim_infs-preserving

      proof

        assume f is continuous;

        then

         A1: f is infs-preserving directed-sups-preserving by Th46;

        let N be net of S;

        set M = (f * N);

        set Y = the set of all ( "/\" ({ (M . i) where i be Element of M : i >= j },T)) where j be Element of M;

        reconsider X = the set of all ( "/\" ({ (N . i) where i be Element of N : i >= j },S)) where j be Element of N as directed non empty Subset of S by Th25;

        

         A2: ex_sup_of (X,S) by YELLOW_0: 17;

        

         A3: f preserves_sup_of X by A1;

        

         A4: the RelStr of (f * N) = the RelStr of N by WAYBEL_9:def 8;

        

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

        deffunc A( Element of N) = { (N . i) where i be Element of N : i >= $1 };

        deffunc INF( Element of N) = ( "/\" ( A($1),S));

        defpred P[ set] means not contradiction;

        

         A6: (f .: { INF(i) where i be Element of N : P[i] }) = { (f . INF(i)) where i be Element of N : P[i] } from LATTICE3:sch 2( A5);

        

         A7: (f .: X) = Y

        proof

           A8:

          now

            let j be Element of N;

            let j9 be Element of M such that

             A9: j9 = j;

            defpred Q[ Element of N] means $1 >= j;

            defpred Q9[ Element of M] means $1 >= j9;

            deffunc F( Element of N) = (f . (N . $1));

            deffunc G( set) = (f . (the mapping of N . $1));

            

             A10: for v be Element of N st Q[v] holds F(v) = G(v);

            deffunc H( set) = ((f * the mapping of N) . $1);

            deffunc I( Element of M) = (M . $1);

            

             A11: for v be Element of N st Q[v] holds G(v) = H(v) by FUNCT_2: 15;

            

             A12: for v be Element of M st Q9[v] holds H(v) = I(v) by WAYBEL_9:def 8;

            defpred P[ set] means [j9, $1] in the InternalRel of N;

            

             A13: for v be Element of N holds Q[v] iff P[v] by A9, ORDERS_2:def 5;

            

             A14: for v be Element of M holds P[v] iff Q9[v] by A4, ORDERS_2:def 5;

            deffunc N( Element of N) = (N . $1);

            

            thus (f .: A(j)) = (f .: { N(i) where i be Element of N : Q[i] })

            .= { (f . N(k)) where k be Element of N : Q[k] } from LATTICE3:sch 2( A5)

            .= { F(k) where k be Element of N : Q[k] }

            .= { G(s) where s be Element of N : Q[s] } from FRAENKEL:sch 6( A10)

            .= { H(o) where o be Element of N : Q[o] } from FRAENKEL:sch 6( A11)

            .= { H(r) where r be Element of N : P[r] } from FRAENKEL:sch 3( A13)

            .= { H(m) where m be Element of M : P[m] } by A4

            .= { H(q) where q be Element of M : Q9[q] } from FRAENKEL:sch 3( A14)

            .= { I(n) where n be Element of M : Q9[n] } from FRAENKEL:sch 6( A12)

            .= { (M . n) where n be Element of M : n >= j9 };

          end;

           A15:

          now

            let j be Element of N;

             A(j) c= the carrier of S

            proof

              let b be object;

              assume b in A(j);

              then ex i be Element of N st b = (N . i) & i >= j;

              hence thesis;

            end;

            then

            reconsider A = A(j) as Subset of S;

            

             A16: f preserves_inf_of A by A1;

             ex_inf_of (A,S) by YELLOW_0: 17;

            hence (f . ( "/\" ( A(j),S))) = ( "/\" ((f .: A(j)),T)) by A16;

          end;

          thus (f .: X) c= Y

          proof

            let a be object;

            assume a in (f .: X);

            then

            consider j be Element of N such that

             A17: a = (f . ( "/\" ({ (N . i) where i be Element of N : i >= j },S))) by A6;

            

             A18: a = ( "/\" ((f .: A(j)),T)) by A15, A17;

            reconsider j9 = j as Element of M by A4;

            (f .: A(j)) = { (M . n) where n be Element of M : n >= j9 } by A8;

            hence thesis by A18;

          end;

          let a be object;

          assume a in Y;

          then

          consider j9 be Element of M such that

           A19: a = ( "/\" ({ (M . n) where n be Element of M : n >= j9 },T));

          reconsider j = j9 as Element of N by A4;

          a = ( "/\" ((f .: A(j)),T)) by A8, A19

          .= (f . ( "/\" ( A(j),S))) by A15;

          hence thesis by A6;

        end;

        

        thus (f . ( lim_inf N)) = (f . ( sup X)) by WAYBEL11:def 6

        .= ( sup (f .: X)) by A2, A3

        .= ( lim_inf (f * N)) by A7, WAYBEL11:def 6;

      end;

      assume

       A20: for N be net of S holds (f . ( lim_inf N)) = ( lim_inf (f * N));

      

       A21: f is directed-sups-preserving

      proof

        let D be Subset of S;

        assume D is non empty directed;

        then

        reconsider D9 = D as non empty directed Subset of S;

        assume ex_sup_of (D,S);

        thus ex_sup_of ((f .: D),T) by YELLOW_0: 17;

        

        thus (f . ( sup D)) = (f . ( lim_inf ( Net-Str D9))) by WAYBEL17: 10

        .= ( lim_inf (f * ( Net-Str D9))) by A20

        .= ( sup (f .: D)) by Th33;

      end;

      

       A22: for X be finite Subset of S holds f preserves_inf_of X by Def1;

      now

        let X be non empty filtered Subset of S;

        reconsider fX = (f .: X) as filtered non empty Subset of T by WAYBEL20: 24;

        thus f preserves_inf_of X

        proof

          assume ex_inf_of (X,S);

          thus ex_inf_of ((f .: X),T) by YELLOW_0: 17;

          (f . ( inf X)) = (f . ( lim_inf (X opp+id ))) by Th28

          .= ( lim_inf (f * (X opp+id ))) by A20

          .= ( inf fX) by Th29

          .= ( lim_inf (fX opp+id )) by Th28;

          hence thesis by Th28;

        end;

      end;

      then f is infs-preserving by A22, WAYBEL_0: 71;

      hence thesis by A21, Th46;

    end;

    theorem :: WAYBEL21:48

    

     Th48: for T be Lawson complete continuous TopLattice holds for S be meet-inheriting full non empty SubRelStr of T st ( Top T) in the carrier of S & ex X be Subset of T st X = the carrier of S & X is closed holds S is infs-inheriting

    proof

      let T be Lawson complete continuous TopLattice;

      let S be meet-inheriting full non empty SubRelStr of T such that

       A1: ( Top T) in the carrier of S;

      given X be Subset of T such that

       A2: X = the carrier of S and

       A3: X is closed;

      S is filtered-infs-inheriting

      proof

        let Y be filtered Subset of S;

        assume Y <> {} ;

        then

        reconsider F = Y as filtered non empty Subset of T by YELLOW_2: 7;

        set N = (F opp+id );

        assume ex_inf_of (Y,T);

        the mapping of N = ( id Y) by WAYBEL19: 27;

        then

         A4: ( rng the mapping of N) = Y;

        ( Lim N) = {( inf F)} by WAYBEL19: 43;

        then {( inf F)} c= ( Cl X) by A2, A4, Th27, WAYBEL19: 26;

        then {( inf F)} c= X by A3, PRE_TOPC: 22;

        hence thesis by A2, ZFMISC_1: 31;

      end;

      hence thesis by A1, Th16;

    end;

    theorem :: WAYBEL21:49

    

     Th49: for T be Lawson complete continuous TopLattice holds for S be full non empty SubRelStr of T st ex X be Subset of T st X = the carrier of S & X is closed holds S is directed-sups-inheriting

    proof

      let T be Lawson complete continuous TopLattice;

      let S be full non empty SubRelStr of T;

      given X be Subset of T such that

       A1: X = the carrier of S and

       A2: X is closed;

      let Y be directed Subset of S;

      assume Y <> {} ;

      then

      reconsider D = Y as directed non empty Subset of T by YELLOW_2: 7;

      set N = ( Net-Str D);

      assume ex_sup_of (Y,T);

      the mapping of N = ( id Y) by Th32;

      then ( rng the mapping of N) = Y;

      then ( Lim N) c= ( Cl X) by A1, Th27, WAYBEL19: 26;

      then

       A3: ( Lim N) c= X by A2, PRE_TOPC: 22;

      ( sup D) in ( Lim N) by Th35;

      hence thesis by A1, A3;

    end;

    theorem :: WAYBEL21:50

    

     Th50: for T be Lawson complete continuous TopLattice holds for S be infs-inheriting directed-sups-inheriting full non empty SubRelStr of T holds ex X be Subset of T st X = the carrier of S & X is closed

    proof

      let T be Lawson complete continuous TopLattice;

      let S be infs-inheriting directed-sups-inheriting full non empty SubRelStr of T;

      reconsider X = the carrier of S as Subset of T by YELLOW_0:def 13;

      take X;

      thus X = the carrier of S;

      reconsider S as complete CLSubFrame of T by Th18;

      set SL = the Lawson correct TopAugmentation of S;

      

       A1: the RelStr of SL = the RelStr of S by YELLOW_9:def 4;

      set f = ( incl (SL,T)), f9 = ( incl (S,T));

      

       A2: the carrier of S c= the carrier of T by YELLOW_0:def 13;

      then

       A3: f = ( id the carrier of SL) by A1, YELLOW_9:def 1;

      

       A4: f9 = ( id the carrier of SL) by A1, A2, YELLOW_9:def 1;

      

       A5: ( [#] SL) is compact by COMPTS_1: 1;

      

       A6: f9 is infs-preserving by Th8;

       the RelStr of T = the RelStr of T;

      then

       A7: f is infs-preserving directed-sups-preserving by A1, A3, A4, A6, Th6, Th10;

      then f is SemilatticeHomomorphism of SL, T by Th5;

      then f is continuous by A7, Th46;

      then (f .: ( [#] SL)) is compact by A5, WEIERSTR: 8;

      then X is compact by A1, A3, FUNCT_1: 92;

      hence thesis by COMPTS_1: 7;

    end;

    theorem :: WAYBEL21:51

    

     Th51: for T be Lawson complete continuous TopLattice holds for S be infs-inheriting directed-sups-inheriting full non empty SubRelStr of T holds for N be net of T st N is_eventually_in the carrier of S holds ( lim_inf N) in the carrier of S

    proof

      let T be Lawson complete continuous TopLattice;

      let S be infs-inheriting directed-sups-inheriting full non empty SubRelStr of T;

      set X = the carrier of S;

      let N be net of T;

      assume N is_eventually_in X;

      then

      consider a be Element of N such that (N . a) in X and

       A1: ( rng the mapping of (N | a)) c= X by Th42;

      deffunc up( Element of (N | a)) = { ((N | a) . i) where i be Element of (N | a) : i >= $1 };

      reconsider iN = the set of all ( "/\" ( up(j),T)) where j be Element of (N | a) as directed non empty Subset of T by Th25;

      iN c= X

      proof

        let z be object;

        assume z in iN;

        then

        consider j be Element of (N | a) such that

         A2: z = ( "/\" ( up(j),T));

         up(j) c= X

        proof

          let u be object;

          assume u in up(j);

          then ex i be Element of (N | a) st (u = ((N | a) . i)) & (i >= j);

          then u in ( rng the mapping of (N | a)) by FUNCT_2: 4;

          hence thesis by A1;

        end;

        then

        reconsider Xj = up(j) as Subset of S;

         ex_inf_of (Xj,T) by YELLOW_0: 17;

        hence thesis by A2, YELLOW_0:def 18;

      end;

      then

      reconsider jN = iN as non empty Subset of S;

      

       A3: jN is directed by WAYBEL10: 23;

       ex_sup_of (jN,T) by YELLOW_0: 17;

      then ( "\/" (jN,T)) in the carrier of S by A3, WAYBEL_0:def 4;

      then ( lim_inf (N | a)) in X by WAYBEL11:def 6;

      hence thesis by Th41;

    end;

    theorem :: WAYBEL21:52

    

     Th52: for T be Lawson complete continuous TopLattice holds for S be meet-inheriting full non empty SubRelStr of T st ( Top T) in the carrier of S & for N be net of T st ( rng the mapping of N) c= the carrier of S holds ( lim_inf N) in the carrier of S holds S is infs-inheriting

    proof

      let T be Lawson complete continuous TopLattice;

      let S be meet-inheriting full non empty SubRelStr of T such that

       A1: ( Top T) in the carrier of S;

      set X = the carrier of S;

      assume

       A2: for N be net of T st ( rng the mapping of N) c= X holds ( lim_inf N) in X;

      S is filtered-infs-inheriting

      proof

        let Y be filtered Subset of S;

        assume Y <> {} ;

        then

        reconsider F = Y as non empty filtered Subset of T by YELLOW_2: 7;

        assume ex_inf_of (Y,T);

        the mapping of (F opp+id ) = ( id F) by WAYBEL19: 27;

        then

         A3: ( rng the mapping of (F opp+id )) = Y;

        ( lim_inf (F opp+id )) = ( inf F) by Th28;

        hence thesis by A2, A3;

      end;

      hence thesis by A1, Th16;

    end;

    theorem :: WAYBEL21:53

    

     Th53: for T be Lawson complete continuous TopLattice holds for S be full non empty SubRelStr of T st for N be net of T st ( rng the mapping of N) c= the carrier of S holds ( lim_inf N) in the carrier of S holds S is directed-sups-inheriting

    proof

      let T be Lawson complete continuous TopLattice;

      let S be full non empty SubRelStr of T;

      set X = the carrier of S;

      assume

       A1: for N be net of T st ( rng the mapping of N) c= X holds ( lim_inf N) in X;

      let Y be directed Subset of S;

      assume Y <> {} ;

      then

      reconsider F = Y as non empty directed Subset of T by YELLOW_2: 7;

      assume ex_sup_of (Y,T);

      the mapping of ( Net-Str F) = ( id F) by Th32;

      then

       A2: ( rng the mapping of ( Net-Str F)) = Y;

      ( lim_inf ( Net-Str F)) = ( sup F) by WAYBEL17: 10;

      hence thesis by A1, A2;

    end;

    theorem :: WAYBEL21:54

    for T be Lawson complete continuous TopLattice holds for S be meet-inheriting full non empty SubRelStr of T holds for X be Subset of T st X = the carrier of S & ( Top T) in X holds X is closed iff for N be net of T st N is_eventually_in X holds ( lim_inf N) in X

    proof

      let T be Lawson complete continuous TopLattice;

      let S be meet-inheriting full non empty SubRelStr of T;

      let X be Subset of T such that

       A1: X = the carrier of S and

       A2: ( Top T) in X;

      hereby

        assume X is closed;

        then S is infs-inheriting directed-sups-inheriting full non empty SubRelStr of T by A1, A2, Th48, Th49;

        hence for N be net of T st N is_eventually_in X holds ( lim_inf N) in X by A1, Th51;

      end;

      assume for N be net of T st N is_eventually_in X holds ( lim_inf N) in X;

      then for N be net of T st ( rng the mapping of N) c= the carrier of S holds ( lim_inf N) in the carrier of S by A1, Th27;

      then S is infs-inheriting directed-sups-inheriting by A1, A2, Th52, Th53;

      then ex X be Subset of T st X = the carrier of S & X is closed by Th50;

      hence thesis by A1;

    end;