The Mizar article:

Lawson Topology in Continuous Lattices

by
Grzegorz Bancerek

Received July 12, 1998

Copyright (c) 1998 Association of Mizar Users

MML identifier: WAYBEL21
[ MML identifier index ]


environ

 vocabulary WAYBEL_0, LATTICES, PRE_TOPC, FINSET_1, FUNCOP_1, YELLOW_0, BOOLE,
      RELAT_1, FUNCT_1, ORDINAL2, SEQM_3, LATTICE3, ORDERS_1, QUANTAL1, BHSP_3,
      CAT_1, FUNCT_3, WELLORD1, WAYBEL_5, CONNSP_2, TOPS_1, RELAT_2, WAYBEL_9,
      OPPCAT_1, SUBSET_1, WAYBEL19, YELLOW_6, WAYBEL11, CANTOR_1, YELLOW_9,
      PROB_1, YELLOW_2, PRELAMB, COMPTS_1, WAYBEL21;
 notation TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FINSET_1,
      TOLER_1, STRUCT_0, PRE_TOPC, TOPS_1, CONNSP_2, COMPTS_1, CANTOR_1,
      ORDERS_1, LATTICE3, ORDERS_3, YELLOW_0, YELLOW_2, WAYBEL_0, WAYBEL_3,
      WAYBEL_5, YELLOW_6, YELLOW_7, BORSUK_1, WAYBEL_9, YELLOW_9, WAYBEL11,
      WAYBEL17, WAYBEL19;
 constructors TOLER_1, ORDERS_3, WAYBEL_1, CANTOR_1, TOPS_1, WAYBEL_3,
      NATTRA_1, URYSOHN1, YELLOW_9, WAYBEL19, WAYBEL17, MEMBERED, PARTFUN1;
 clusters STRUCT_0, YELLOW_0, RELSET_1, LATTICE3, WAYBEL_0, FINSET_1, PUA2MSS1,
      YELLOW_6, WAYBEL_2, WAYBEL_9, WAYBEL10, WAYBEL17, YELLOW_9, WAYBEL19,
      SUBSET_1, MEMBERED, RELAT_1, ZFMISC_1, FUNCT_2, PARTFUN1;
 requirements SUBSET, BOOLE;
 definitions TARSKI, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_1, YELLOW_6,
      XBOOLE_0;
 theorems YELLOW_0, WAYBEL_0, WAYBEL_6, PRE_TOPC, FUNCOP_1, RELAT_1, BORSUK_1,
      FUNCT_2, TOPS_1, TOPS_2, ZFMISC_1, CONNSP_2, WAYBEL_9, YELLOW_9, FUNCT_1,
      WAYBEL_1, YELLOW_6, WAYBEL19, WELLORD1, SETWISEO, FUNCT_3, TARSKI,
      CANTOR_1, LATTICE3, FINSET_1, WAYBEL11, WAYBEL17, ORDERS_1, YELLOW_2,
      WEIERSTR, COMPTS_1, WAYBEL10, YELLOW_7, YELLOW_4, WAYBEL20, RELSET_1,
      XBOOLE_0, XBOOLE_1;
 schemes FRAENKEL, FINSET_1, LATTICE3, XBOOLE_0;

begin :: Semilattice homomorphism and inheritance

definition
 let S,T be Semilattice such that
A1:   S is upper-bounded implies T is upper-bounded;
 mode SemilatticeHomomorphism of S,T -> map of S,T means:
Def1:
  for X being finite Subset of S holds it preserves_inf_of X;
 existence
  proof
   reconsider f = (the carrier of S) --> Top T as map of S,T;
   take f; let X be finite Subset of S such that
A2:  ex_inf_of X,S;
   per cases; suppose X = {};
then A3:  f.:X = {} & S is upper-bounded by A2,RELAT_1:149,WAYBEL20:5;
    hence ex_inf_of f.:X,T by A1,YELLOW_0:43;
    thus f.inf X = Top T by FUNCOP_1:13 .= inf (f.:X) by A3,YELLOW_0:def 12;
   suppose X <> {};
    then reconsider A = X as non empty Subset of S;
    consider a being Element of A;
    reconsider a as Element of S;
       dom f = the carrier of S & f.a = Top T by FUNCOP_1:13,19;
     then Top T in f.:X by FUNCT_1:def 12;
     then {Top T} c= f.:X & f.:X c= {Top T} by BORSUK_1:6,ZFMISC_1:37;
     then {Top T} = f.:X & f.inf X = Top T by FUNCOP_1:13,XBOOLE_0:def 10;
    hence thesis by YELLOW_0:38,39;
  end;
end;

definition
 let S,T be Semilattice;
 cluster meet-preserving -> monotone map of S,T;
 coherence
  proof let f be map 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;

definition
 let S be Semilattice, T be upper-bounded Semilattice;
 cluster -> meet-preserving SemilatticeHomomorphism of S,T;
 coherence
  proof let f be SemilatticeHomomorphism of S,T;
   let x,y be Element of S; thus f preserves_inf_of {x,y} by Def1;
  end;
end;

theorem
   for S,T being upper-bounded Semilattice
 for f being 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;
      f preserves_inf_of {}S & ex_inf_of {}S,S by Def1,YELLOW_0:43;
    then f.inf {}S = inf (f.:{}S) by WAYBEL_0:def 30;
   hence f.Top S = inf (f.:{}S) by YELLOW_0:def 12 .= inf {}T by RELAT_1:149
             .= Top T by YELLOW_0:def 12;
  end;

theorem Th2:
 for S,T being Semilattice, f being map of S,T st f is meet-preserving
 for X being finite non empty Subset of S holds f preserves_inf_of X
   proof
    let S,T be Semilattice, f be map 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 & x c= X & P[x];
      thus P[x \/ {y}]
       proof assume x \/ {y} <> {};
      reconsider y' = y as Element of S by A5;
      set fy = f.y';
A6:    ex_inf_of {fy}, T & inf {fy} = fy &
       ex_inf_of {y'}, S & inf {y'} = y by YELLOW_0:38,39;
      hence ex_inf_of x \/ {y}, S by A5,YELLOW_2:4;
    A7: dom f = the carrier of S by FUNCT_2:def 1;
then f.:{y} = {fy} by FUNCT_1:117;
then A8:    f.:(x \/ {y}) = (f.:x) \/ {fy} by RELAT_1:153;
      hence ex_inf_of f.:(x \/ {y}), T by A5,A6,A7,FUNCT_1:117,YELLOW_2:4;
      per cases; suppose x = {};
      hence "/\"(f.:(x \/ {y}), T) = f."/\"(x \/ {y}, S) by A6,A7,FUNCT_1:117;
      suppose
A9:    x <> {};
      hence "/\"(f.:(x \/ {y}), T)
          = (f."/\"(x, S)) "/\" fy by A5,A6,A8,YELLOW_2:4
         .= f.("/\"(x, S)"/\" y') by A1,WAYBEL_6:1
         .= f."/\"(x \/ {y}, S) by A5,A6,A9,YELLOW_2:4;
      end;
     end;
    P[X] from Finite(A2,A3,A4);
    hence thesis;
   end;

theorem
   for S,T being upper-bounded Semilattice, f being meet-preserving map 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 map 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;
       f.:{} = {} & Top S = "/\"({},S) by RELAT_1:149,YELLOW_0:def 12;
then A2:  ex_inf_of f.:{}, T & "/\"(f.:{}, T) = f."/\"
({}, S) by A1,YELLOW_0:43,def 12;
       X = {} or f preserves_inf_of X by Th2;
    hence thesis by A2,WAYBEL_0:def 30;
   end;

theorem Th4:
 for S,T being Semilattice, f being map of S,T
  st f is meet-preserving &
     for X being filtered non empty Subset of S holds f preserves_inf_of X
 for X being non empty Subset of S holds f preserves_inf_of X
  proof let S,T be Semilattice, f be map of S,T
   such that
A1: f is meet-preserving and
A2: for X being 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[set] means
    ex Y being non empty finite Subset of X st ex_inf_of Y, S & $1 = "/\"(Y,S);
   consider Z being set such that
A4: for x being set holds x in Z iff x in the carrier of S & P[x]
      from Separation;
   consider a being Element of X;
    A5: ex_inf_of {a}, S & inf {a} = a & {a} c= X
     by YELLOW_0:38,39,ZFMISC_1:37;
      Z c= the carrier of S proof let x be set; thus thesis by A4; end;
   then reconsider Z as non empty Subset of S by A4,A5;
A6: now let Y be finite Subset of X;
        Y is Subset of S by XBOOLE_1:1;
      then Y is finite Subset of S;
     hence Y <> {} implies ex_inf_of Y, S by YELLOW_0:55;
    end;
A7: now let Y be finite Subset of X;
        Y is Subset of S by XBOOLE_1:1;
     then reconsider Y' = Y as Subset of S;
     assume
A8:    Y <> {};
      then ex_inf_of Y', S by YELLOW_0:55;
     hence "/\"(Y,S) in Z by A4,A8;
    end;
      now let x be Element of S; assume x in Z;
      then ex Y being non empty finite Subset of X st ex_inf_of Y,S & x = "/\"
(Y,S)
       by A4;
     hence ex Y being finite Subset of X st ex_inf_of Y,S & x = "/\"(Y,S);
    end;
then A9: Z is filtered & ex_inf_of Z, S & inf Z = inf X & Z <> {}
     by A3,A6,A7,WAYBEL_0:56,58,59;
    then f preserves_inf_of Z by A2;
then A10: ex_inf_of f.:Z,T & inf (f.:Z) = f.inf Z & inf Z = inf X
     by A9,WAYBEL_0:def 30;
      X c= Z
     proof let x be set; assume
A11:     x in X;
      then reconsider Y = {x} as finite Subset of X by ZFMISC_1:37;
      reconsider x as Element of S by A11;
         Y is Subset of S by XBOOLE_1:1;
       then Y is Subset of S;
       then ex_inf_of Y, S & x = "/\"(Y,S) by YELLOW_0:39,55;
      hence thesis by A4;
     end;
then A12: f.:X c= f.:Z by RELAT_1:156;
A13: f.:Z is_>=_than f.inf X by A10,YELLOW_0:31;
A14: f.:X is_>=_than f.inf X
     proof let x be Element of T; assume x in f.:X;
      hence thesis by A12,A13,LATTICE3:def 8;
     end;
A15: now let b be Element of T; assume
A16:  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 being set such that
A17:     x in dom f & x in Z & a = f.x by FUNCT_1:def 12;
        consider Y being non empty finite Subset of X such that
A18:     ex_inf_of Y, S & x = "/\"(Y,S) by A4,A17;
           Y is Subset of S by XBOOLE_1:1;
        then reconsider Y as Subset of S;
           f.:Y c= f.:X & f preserves_inf_of Y by A1,Th2,RELAT_1:156;
         then b is_<=_than f.:Y & a = "/\"(f.:Y,T) & ex_inf_of f.:Y, T
          by A16,A17,A18,WAYBEL_0:def 30,YELLOW_0:9;
        hence thesis by YELLOW_0:def 10;
       end;
     hence f.inf X >= b by A10,YELLOW_0:31;
    end;
   hence ex_inf_of f.:X,T by A14,YELLOW_0:16;
   hence inf (f.:X) = f.inf X by A14,A15,YELLOW_0:def 10;
  end;


theorem Th5:
 for S,T being Semilattice, f being map of S,T st f is infs-preserving
  holds f is SemilatticeHomomorphism of S,T
  proof let S,T be Semilattice, f be map of S,T such that
A1:  f is infs-preserving;
      {} c= the carrier of S by XBOOLE_1:2;
   then reconsider e = {} as Subset of S;
   hereby assume S is upper-bounded;
     then ex_inf_of e, S & f preserves_inf_of e
      by A1,WAYBEL_0:def 32,YELLOW_0:43;
     then ex_inf_of f.:e, T & f.:e = {} by RELAT_1:149,WAYBEL_0:def 30;
    hence T is upper-bounded by WAYBEL20:5;
   end;
   let X be finite Subset of S; thus thesis by A1,WAYBEL_0:def 32;
  end;

theorem Th6:
 for S1,T1,S2,T2 being non empty RelStr
  st the RelStr of S1 = the RelStr of S2 & the RelStr of T1 = the RelStr of T2
 for f1 being map of S1,T1, f2 being map 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 & the RelStr of T1 = the RelStr of T2;
   let f1 be map of S1,T1, f2 be map of S2,T2 such that
A2:  f1 = f2;
   thus f1 is infs-preserving implies f2 is infs-preserving
    proof assume
A3:    for X being Subset of S1 holds f1 preserves_inf_of X;
     let X be Subset of S2;
     reconsider Y = X as Subset of S1 by A1;
        f1 preserves_inf_of Y by A3;
     hence thesis by A1,A2,WAYBEL_0:65;
    end;
   assume
A4:  for X being 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 Y is non empty directed by A1,WAYBEL_0:3;
     then f1 preserves_sup_of Y by A4;
    hence thesis by A1,A2,WAYBEL_0:65;
  end;

theorem
   for S1,T1,S2,T2 being non empty RelStr
  st the RelStr of S1 = the RelStr of S2 & the RelStr of T1 = the RelStr of T2
 for f1 being map of S1,T1, f2 being map 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 & the RelStr of T1 = the RelStr of T2;
   let f1 be map of S1,T1, f2 be map of S2,T2 such that
A2:  f1 = f2;
   thus f1 is sups-preserving implies f2 is sups-preserving
    proof assume
A3:    for X being Subset of S1 holds f1 preserves_sup_of X;
     let X be Subset of S2;
     reconsider Y = X as Subset of S1 by A1;
        f1 preserves_sup_of Y by A3;
     hence thesis by A1,A2,WAYBEL_0:65;
    end;
   assume
A4:  for X being 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 Y is non empty filtered by A1,WAYBEL_0:4;
     then f1 preserves_inf_of Y by A4;
    hence thesis by A1,A2,WAYBEL_0:65;
  end;

theorem Th8:
 for T being complete LATTICE
 for S being 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 f = id the carrier of S by YELLOW_9:def 1;
then A1: f.:X = X & ex_inf_of X, T & f.inf X = inf X
     by BORSUK_1:3,FUNCT_1:35,YELLOW_0:17;
     then "/\"(X,T) in the carrier of S by YELLOW_0:def 18;
     hence thesis by A1,YELLOW_0:64;
  end;

theorem
   for T being complete LATTICE
 for S being 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 f = id the carrier of S by YELLOW_9:def 1;
then A1: f.:X = X & ex_sup_of X, T & f.sup X = sup X
     by BORSUK_1:3,FUNCT_1:35,YELLOW_0:17;
     then "\/"(X,T) in the carrier of S by YELLOW_0:def 19;
   hence thesis by A1,YELLOW_0:65;
  end;

theorem Th10:
 for T being up-complete (non empty Poset)
 for S being 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
A1:  X is non empty directed & ex_sup_of X, S;
   then reconsider X' = X as non empty directed Subset of T by YELLOW_2:7;
      the carrier of S c= the carrier of T by YELLOW_0:def 13;
    then f = id the carrier of S by YELLOW_9:def 1;
then A2:  f.:X = X' & f.sup X = sup X by BORSUK_1:3,FUNCT_1:35;
   hence ex_sup_of f.:X, T by WAYBEL_0:75;
   hence thesis by A1,A2,WAYBEL_0:7;
  end;

theorem
   for T being complete LATTICE
 for S being 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
A1:  X is non empty filtered & 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 f = id the carrier of S by YELLOW_9:def 1;
    then f.:X = X & ex_inf_of X, T & f.inf X = inf X
     by BORSUK_1:3,FUNCT_1:35,YELLOW_0:17;
   hence thesis by A1,WAYBEL_0:6;
  end;

theorem Th12:
 for T1,T2,R being RelStr, S being 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 & the RelStr of S = the RelStr of R;
   thus
A2:  R is SubRelStr of T2
     proof thus the carrier of R c= the carrier of T2 &
       the InternalRel of R c= the InternalRel of T2 by A1,YELLOW_0:def 13;
     end;
   assume the InternalRel of S = (the InternalRel of T)|_2 the carrier of S;
   hence thesis by A1,A2,YELLOW_0:def 14;
  end;

theorem Th13:
 for T being 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:15;
A1:  R is infs-inheriting
     proof let X be Subset of R;
      thus thesis;
     end;
      R is sups-inheriting
     proof let X be Subset of R;
      thus thesis;
     end;
   hence thesis by A1;
  end;

definition
 let T be complete LATTICE;
 cluster complete CLSubFrame of T;
 existence
  proof
      T is infs-inheriting sups-inheriting full SubRelStr of T by Th13;
   hence thesis;
  end;
end;

theorem Th14:
 for T being Semilattice
 for S being full non empty SubRelStr of T
  holds S is meet-inheriting iff
   for X being 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
A5:    y in X & x c= X & P[x];
      thus P[x \/ {y}]
       proof assume x \/ {y} <> {};
        reconsider y' = y as Element of S by A5;
      reconsider z = y' as Element of T by YELLOW_0:59;
         x c= the carrier of S & the carrier of S c= the carrier of T
        by A5,XBOOLE_1:1,YELLOW_0:def 13;
       then x c= the carrier of T by XBOOLE_1:1;
      then reconsider x' = x as finite Subset of T
        by A5,FINSET_1:13;
A6:    ex_inf_of {z}, T & inf {z} = y' by YELLOW_0:38,39;
         now assume
A7:      x' <> {};
         then ex_inf_of x', T by YELLOW_0:55;
then A8:      inf x' in the carrier of S & inf (x' \/ {z}) = (inf x')"/\"z &
         ex_inf_of {inf x', z}, T by A5,A6,A7,YELLOW_0:21,YELLOW_2:4;
         then inf {inf x', z} in the carrier of S by A1,YELLOW_0:def 16;
        hence inf (x' \/ {z}) in the carrier of S by A8,YELLOW_0:40;
       end;
      hence "/\"(x \/ {y}, T) in the carrier of S by A6;
      end;
     end;
       P[X] from Finite(A2,A3,A4);
    hence "/\"(X, T) in the carrier of S;
   end;
   assume
A9:  for X being finite non empty Subset of S holds "/\"
(X, T) in the carrier of S;
   let x,y be Element of T;
   assume x in the carrier of S & y in the carrier of S;
    then {x,y} c= the carrier of S by ZFMISC_1:38;
    then {x,y} is finite non empty Subset of S;
   hence thesis by A9;
  end;

theorem Th15:
 for T being sup-Semilattice
 for S being full non empty SubRelStr of T
  holds S is join-inheriting iff
   for X being 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
A5:    y in X & x c= X & P[x];
      then reconsider y' = y as Element of S;
      reconsider z = y' as Element of T by YELLOW_0:59;
      thus P[x \/ {y}]
      proof assume x \/ {y} <> {};
         x c= the carrier of S & the carrier of S c= the carrier of T
        by A5,XBOOLE_1:1,YELLOW_0:def 13;
       then x c= the carrier of T by XBOOLE_1:1;
      then reconsider x' = x as finite Subset of T
        by A5,FINSET_1:13;
A6:    ex_sup_of {z}, T & sup {z} = y' by YELLOW_0:38,39;
         now assume
A7:      x' <> {};
         then ex_sup_of x', T by YELLOW_0:54;
         then
A8:      sup x' in the carrier of S & sup (x' \/ {z}) = (sup x')"\/"z &
         ex_sup_of {sup x', z}, T by A5,A6,A7,YELLOW_0:20,YELLOW_2:3;
         then sup {sup x', z} in the carrier of S by A1,YELLOW_0:def 17;
        hence sup (x' \/ {z}) in the carrier of S by A8,YELLOW_0:41;
       end;
      hence "\/"(x \/ {y}, T) in the carrier of S by A6;
      end;
     end;
      P[X] from Finite(A2,A3,A4);
    hence "\/"(X, T) in the carrier of S;
   end;
   assume
A9:  for X being finite non empty Subset of S holds "\/"
(X, T) in the carrier of S;
   let x,y be Element of T;
   assume x in the carrier of S & y in the carrier of S;
    then {x,y} c= the carrier of S by ZFMISC_1:38;
    then {x,y} is finite non empty Subset of S;
   hence thesis by A9;
  end;

theorem Th16:
 for T being upper-bounded Semilattice
 for S being 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 & 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 A c= the carrier of T by XBOOLE_1:1;
   then reconsider C = A as Subset of T;
   set F = fininfs C;
   assume
A2:  ex_inf_of A, T;
then A3:  inf F = inf C by WAYBEL_0:60;
A4:  F = {"/\"(Y,T) where Y is finite Subset of C: ex_inf_of Y, T}
     by WAYBEL_0:def 28;
      F c= the carrier of S
     proof let x be set; assume x in F;
      then consider Y being finite Subset of C such that
A5:    x = "/\"(Y, T) & ex_inf_of Y, T by A4;
         Y c= the carrier of T by XBOOLE_1:1;
      then reconsider Y as finite Subset of T;
         Y c= the carrier of S by XBOOLE_1:1;
      then reconsider Z = Y as finite Subset of S;
      assume
A6:    not x in the carrier of S;
       then Z <> {} by A1,A5,YELLOW_0:def 12;
      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:24;
A7: now let Y be finite Subset of C;
        Y c= the carrier of T by XBOOLE_1:1;
      then Y is Subset of T;
     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 being finite Subset of C st x = "/\"(Y,T) & ex_inf_of Y,T by A4
;
     hence ex Y being finite Subset of C st ex_inf_of Y,T & x = "/\"(Y,T);
    end;
      now let Y be finite Subset of C;
        Y c= the carrier of T by XBOOLE_1:1;
     then reconsider Z = Y as finite Subset of T;
     assume Y <> {}; then ex_inf_of Z, T by YELLOW_0:55;
     hence "/\"(Y,T) in F by A4;
    end;
    then ex_inf_of G, T by A2,A7,A8,WAYBEL_0:58;
   hence "/\"(A, T) in the carrier of S by A1,A3,WAYBEL_0:def 3;
  end;

theorem
   for T being lower-bounded sup-Semilattice
 for S being 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 & 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 A c= the carrier of T by XBOOLE_1:1;
   then reconsider C = A as Subset of T;
   set F = finsups C;
   assume
A2:  ex_sup_of A, T;
then A3:  sup F = sup C by WAYBEL_0:55;
A4:  F = {"\/"(Y,T) where Y is finite Subset of C: ex_sup_of Y, T}
     by WAYBEL_0:def 27;
      F c= the carrier of S
     proof let x be set; assume x in F;
      then consider Y being finite Subset of C such that
A5:    x = "\/"(Y, T) & ex_sup_of Y, T by A4;
         Y c= the carrier of T by XBOOLE_1:1;
      then reconsider Y as finite Subset of T;
         Y c= the carrier of S by XBOOLE_1:1;
      then reconsider Z = Y as finite Subset of S;
      assume
A6:    not x in the carrier of S;
       then Z <> {} by A1,A5,YELLOW_0:def 11;
      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:24;
A7: now let Y be finite Subset of C;
        Y c= the carrier of T by XBOOLE_1:1;
      then Y is Subset of T;
     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 being finite Subset of C st x = "\/"(Y,T) & ex_sup_of Y,T by A4
;
     hence ex Y being finite Subset of C st ex_sup_of Y,T & x = "\/"(Y,T);
    end;
      now let Y be finite Subset of C;
        Y c= the carrier of T by XBOOLE_1:1;
     then reconsider Z = Y as finite Subset of T;
     assume Y <> {}; then ex_sup_of Z, T by YELLOW_0:54;
     hence "\/"(Y,T) in F by A4;
    end;
    then ex_sup_of G, T by A2,A7,A8,WAYBEL_0:53;
   hence "\/"(A, T) in the carrier of S by A1,A3,WAYBEL_0:def 4;
  end;

theorem Th18:
 for T being complete LATTICE, S being 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;
        Y c= the carrier of S by XBOOLE_1:17;
     then reconsider Y as Subset of S;
A2:   ex_inf_of Y, T by YELLOW_0:17;
     then "/\"(Y,T) in the carrier of S by A1,YELLOW_0:def 18;
      then ex_inf_of Y, S by A2,YELLOW_0:64;
     hence ex_inf_of X, S by YELLOW_0:50;
    end;
   hence thesis by YELLOW_2:27;
  end;

theorem
   for T being complete LATTICE, S being 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;
        Y c= the carrier of S by XBOOLE_1:17;
     then reconsider Y as Subset of S;
A2:  ex_sup_of Y, T by YELLOW_0:17;
     then "\/"(Y,T) in the carrier of S by A1,YELLOW_0:def 19;
      then ex_sup_of Y, S by A2,YELLOW_0:65;
     hence ex_sup_of X, S by YELLOW_0:50;
    end;
   hence thesis by YELLOW_2:26;
  end;

theorem
   for T1,T2 being non empty RelStr
 for S1 being non empty full SubRelStr of T1
 for S2 being 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 being 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 ex_inf_of Y,T1 by A1,YELLOW_0:14;
    then "/\"(Y,T1) in the carrier of S1 by A3;
   hence thesis by A1,A2,A4,YELLOW_0:27;
  end;

theorem
   for T1,T2 being non empty RelStr
 for S1 being non empty full SubRelStr of T1
 for S2 being 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 being 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 ex_sup_of Y,T1 by A1,YELLOW_0:14;
    then "\/"(Y,T1) in the carrier of S1 by A3;
   hence thesis by A1,A2,A4,YELLOW_0:26;
  end;

theorem
   for T1,T2 being non empty RelStr
 for S1 being non empty full SubRelStr of T1
 for S2 being 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:58;
   assume
A4:  for X being 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 ex_sup_of Y,T1 by A1,YELLOW_0:14;
    then "\/"(Y,T1) in the carrier of S1 by A4,A5;
   hence thesis by A1,A2,A6,YELLOW_0:26;
  end;

theorem
   for T1,T2 being non empty RelStr
 for S1 being non empty full SubRelStr of T1
 for S2 being 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:58;
   assume
A4:  for X being 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 ex_inf_of Y,T1 by A1,YELLOW_0:14;
    then "/\"(Y,T1) in the carrier of S1 by A4,A5;
   hence thesis by A1,A2,A6,YELLOW_0:27;
  end;

begin :: Nets and limits

theorem Th24:
 for S,T being non empty TopSpace, N being net of S
 for f being map 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;
   let f be map of S,T such that
A1:  f is continuous;
   let p be set; assume
A2:  p in f.:Lim N; then reconsider p as Point of T;
   consider x being set such that
A3:  x in the carrier of S & x in Lim N & p = f.x by A2,FUNCT_2:115;
   reconsider x as Element of S by A3;
      now let V be a_neighborhood of p;
        p in Int V & Int V is open by CONNSP_2:def 1,TOPS_1:51;
      then x in f"Int V & f"Int V is open by A1,A3,FUNCT_2:46,TOPS_2:55;
      then f"Int V is a_neighborhood of x by CONNSP_2:5;
      then N is_eventually_in f"Int V by A3,YELLOW_6:def 18;
     then consider i being Element of N such that
A4:    for j being Element of N st j >= i holds N.j in
 f"Int V by WAYBEL_0:def 11;
A5:    the mapping of f*N = f*the mapping of N &
      the RelStr of f*N = the RelStr of N by WAYBEL_9:def 8;
     then reconsider i' = i as Element of f*N;
     thus f*N is_eventually_in V
      proof take i'; let j' be Element of f*N;
       reconsider j = j' as Element of N by A5;
A6:      f.(N.j) = f.((the mapping of N).j) by WAYBEL_0:def 8
               .= (f*the mapping of N).j by FUNCT_2:21
               .= (f*N).j' by A5,WAYBEL_0:def 8;
       assume j' >= i'; then j >= i by A5,YELLOW_0:1;
        then N.j in f"Int V by A4;
        then f.(N.j) in Int V & Int V c= V by FUNCT_2:46,TOPS_1:44;
       hence thesis by A6;
      end;
    end;
   hence thesis by YELLOW_6:def 18;
  end;

definition
 let T be non empty RelStr;
 let N be non empty NetStr over T;
 redefine attr N is antitone means:
Def2:
  for i,j being Element of N st i <= j holds N.i >= N.j;
  compatibility
   proof
A1:  netmap(N,T) = the mapping of N by WAYBEL_0:def 7;
    hereby assume N is antitone;
then A2:    netmap(N,T) is antitone by WAYBEL_0:def 10;
     let i,j be Element of N; assume i <= j;
      then netmap(N,T).i >= netmap(N,T).j by A2,WAYBEL_0:def 5;
      then N.i >= netmap(N,T).j by A1,WAYBEL_0:def 8;
     hence N.i >= N.j by A1,WAYBEL_0:def 8;
    end;
    assume
A3:   for i,j being Element of N st i <= j holds N.i >= N.j;
    let i,j be Element of N;
       N.i = netmap(N,T).i & N.j = netmap(N,T).j
      by A1,WAYBEL_0:def 8;
    hence thesis by A3;
   end;
end;

definition
 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 & k = x by A1,TARSKI:def 1;
      hence thesis by YELLOW_0:def 1;
     end;
   thus N is directed
     proof let i,j be Element of N; i = x & j = x by A1,TARSKI:def 1;
       then i <= i & j <= i;
      hence thesis;
     end;
   thus N is monotone
     proof let i,j be Element of N; i = x & j = x by A1,TARSKI:def 1;
      hence thesis by YELLOW_0:def 1;
     end;
   let i,j be Element of N; i = x & j = x by A1,TARSKI:def 1;
   hence thesis by YELLOW_0:def 1;
  end;
end;

definition
 let T be non empty reflexive RelStr;
 cluster monotone antitone reflexive strict net of T;
 existence
  proof consider x being Element of T;
   take {x} opp+id; thus thesis;
  end;
end;

definition
 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:59;
   assume i <= j; then x <= y by A1,YELLOW_0:60;
    then ~x >= ~y & ~x = x by LATTICE3:def 7,YELLOW_7:1;
    then (F opp+id).i >= ~y & ~y = y by LATTICE3:def 7,YELLOW_9:7;
   hence (F opp+id).i >= (F opp+id).j by YELLOW_9:7;
  end;
end;

definition
 let S,T be non empty reflexive RelStr;
 let f be monotone map 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 &
    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 A1,YELLOW_0:1;
    then N.x >= N.y by Def2;
    then f.(N.x) >= f.(N.y) & N.x = (the mapping of N).x &
    (f*N).i = (the mapping of f*N).i by WAYBEL_0:def 8,WAYBEL_1:def 2;
    then (f*N).i >= f.(N.y) & N.y = (the mapping of N).y &
    (f*N).j = (the mapping of f*N).j by A1,FUNCT_2:21,WAYBEL_0:def 8;
   hence thesis by A1,FUNCT_2:21;
  end;
end;

theorem Th25:
 for S being complete LATTICE, N be net of S holds
   {"/\"({N.i where i is Element of N:i >= j},S)
       where j is Element of N: not contradiction}
    is directed non empty Subset of S
  proof let S be complete LATTICE, N be net of S;
   set X = {"/\"({N.i where i is Element of N:i >= j},S)
           where j is Element of N: not contradiction};
      X c= the carrier of S
     proof let x be set; assume x in X;
       then ex j being Element of N st
        x = "/\"({N.i where i is 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
   for S being non empty Poset, N be monotone reflexive net of S holds
   {"/\"({N.i where i is Element of N: i >= j}, S)
       where j is Element of N: not contradiction}
    is directed non empty Subset of S
  proof let S be non empty Poset, N be monotone reflexive net of S;
   set X = {"/\"({N.i where i is Element of N: i >= j}, S)
           where j is Element of N: not contradiction};
   consider jj being Element of N;
A1:  "/\"({N.i where i is Element of N: i >= jj}, S) in X;
      X c= the carrier of S
     proof let x be set; assume x in X;
       then ex j being Element of N st
        x = "/\"({N.i where i is 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 being Element of N such that
A2:    x = "/\"({N.i where i is Element of N: i >= j1}, S);
      assume y in X;
      then consider j2 being Element of N such that
A3:    y = "/\"({N.i where i is Element of N: i >= j2}, S);
      reconsider j1,j2 as Element of N;
         [#]N is directed & [#]N = the carrier of N
        by PRE_TOPC:12,WAYBEL_0:def 6;
      then consider j being Element of N such that
A4:    j in [#]N & j >= j1 & j >= j2 by WAYBEL_0:def 1;
      set z = "/\"({N.i where i is Element of N: i >= j}, S);
      take z; thus z in X;
      deffunc up(Element of N)
        = {N.i where i is Element of N: i >= $1};
A5:     for j being Element of N holds ex_inf_of up(j), S
        proof let j be Element of N;
         reconsider j' = j as Element of N;
            now take x = N.j;
              j' <= j';
then A6:         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 being 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 A6,LATTICE3:def 8;
          end;
         hence thesis by YELLOW_0:16;
        end;
then A7:    ex_inf_of up(j1), S;
A8:    ex_inf_of up(j2), S by A5;
A9:    ex_inf_of up(j), S by A5;
      set A = {N.i where i is Element of N:i >= j};
         A c= {N.k where k is Element of N:k >= j1}
        proof let a be set; assume a in A;
         then consider k being Element of N such that
A10:       a = N.k & k >= j;
         reconsider k as Element of N;
            k >= j1 by A4,A10,ORDERS_1:26;
         hence thesis by A10;
        end;
      hence z >= x by A2,A7,A9,YELLOW_0:35;
         A c= {N.k where k is Element of N:k >= j2}
        proof let a be set; assume a in A;
         then consider k being Element of N such that
A11:       a = N.k & k >= j;
         reconsider k as Element of N;
            k >= j2 by A4,A11,ORDERS_1:26;
         hence thesis by A11;
        end;
      hence z >= y by A3,A8,A9,YELLOW_0:35;
     end;
   hence thesis;
  end;

theorem Th27:
 for S being non empty 1-sorted, N being non empty NetStr over S, X being 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;
   consider i being Element of N;
   take i; let j be Element of N;
      N.j = (the mapping of N).j by WAYBEL_0:def 8;
    then N.j in rng the mapping of N by FUNCT_2:6;
   hence thesis by A1;
  end;

theorem Th28:
 for R being /\-complete (non empty Poset)
 for F being 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 is Element of N: i >= $1}, R);
A1: for v being Element of N st P[v] holds F(v) = G(v)
     proof let v be Element of N;
      set X = {N.i where i is 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 set; assume x in X;
         then consider i being Element of N such that
A4:       x = N.i & i >= v;
         reconsider i as Element of N;
            x = i by A4,YELLOW_9:7;
         hence thesis by A2;
        end;
then A5:    X c= the carrier of R by XBOOLE_1:1;
         vv <= vv;
       then N.v in X;
      then reconsider X as non empty Subset of R by A5;
A6:    ex_inf_of F, R & ex_inf_of X, R by WAYBEL_0:76;
then A7:    inf X >= inf F by A3,YELLOW_0:35;
         F is_>=_than inf X
        proof let a be Element of R; assume a in F;
         then consider b being Element of R such that
A8:       b in F & a >= b & j >= b by A2,WAYBEL_0:def 2;
         reconsider k = b as Element of N by A2,A8;
            N is full SubRelStr of R opp & j~ = v & b~ = k & j~ <= b~
           by A8,LATTICE3:9,def 6,YELLOW_9:7;
          then N.k = b & k >= vv by YELLOW_0:61,YELLOW_9:7;
          then b in X;
          then {b} c= X & ex_inf_of {b}, R & inf {b} = b
           by YELLOW_0:38,39,ZFMISC_1:37;
          then b >= inf X by A6,YELLOW_0:35;
         hence thesis by A8,YELLOW_0:def 2;
        end;
       then inf F >= "/\"(X, R) by A6,YELLOW_0:31;
      hence thesis by A7,ORDERS_1:25;
     end;
A9:  {F(j) where j is Element of N: P[j]}
      = {G(k) where k is Element of N: P[k]}
       from FraenkelF'R(A1);
A10: ex j being Element of N st P[j];
      {inf F where j is Element of N: P[j]}
      = {inf F} from SingleFraenkel(A10);
   hence lim_inf N = "\/"({inf F}, R) by A9,WAYBEL11:def 6
     .= inf F by YELLOW_0:39;
  end;

theorem Th29:
 for S,T being /\-complete (non empty Poset)
 for X being non empty filtered Subset of S
 for f being monotone map 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 map of S,T;
   set M = X opp+id, N = f*M;
   deffunc up(Element of N)
     = {N.i where i is Element of N: i >= $1};
   deffunc infy(Element of N) = "/\"(up($1), T);
A1: the RelStr of N = the RelStr of M &
    the mapping of N = f*the mapping of M by WAYBEL_9:def 8;
A2: the carrier of M = X & the mapping of M = id X by WAYBEL19:27,YELLOW_9:7;
   defpred P[set] means not contradiction;
   deffunc G(set) = inf (f.:X);
A3:  for j being Element of N st P[j] holds infy(j) = G(j)
     proof let j be Element of N;
      reconsider j as Element of N;
A4:    [#]N is directed & [#]N = the carrier of N
        by PRE_TOPC:12,WAYBEL_0:def 6;
      then consider i' being Element of N such that
A5:    i' in [#]N & i' >= j & i' >= j by WAYBEL_0:def 1;
A6:    up(j) c= f.:X
        proof let a be set; assume a in up(j);
         then consider i being Element of N such that
A7:       a = N.i & i >= j;
         reconsider i as Element of N;
         reconsider i' = i as Element of M by A1;
A8:       N.i = (the mapping of N).i by WAYBEL_0:def 8
             .= f.((id X).i) by A1,A2,FUNCT_2:21
             .= f.i' by A2,FUNCT_1:35;
            i' in X & the carrier of T <> {} by A2;
         hence thesis by A7,A8,FUNCT_2:43;
        end;
       then up(j) c= the carrier of T & N.i' in up(j) by A5,XBOOLE_1:1;
       then up(j) is non empty Subset of T;
then A9:    ex_inf_of up(j), T & ex_inf_of f.:X, T by WAYBEL_0:76;
then A10:    infy(j) >= inf (f.:X) by A6,YELLOW_0:35;
         infy(j) is_<=_than f.:X
        proof let x be Element of T; assume x in f.:X;
         then consider y being set such that
A11:       y in the carrier of S & y in X & x = f.y by FUNCT_2:115;
         reconsider y as Element of N by A1,A2,A11;
         consider i being Element of N such that
A12:       i in [#]N & i >= y & i >= j by A4,WAYBEL_0:def 1;
            i in X by A1,A2;
         then reconsider xi = i, xy = y as Element of S by A11;
            M is full SubRelStr of S opp by YELLOW_9:7;
          then N is full SubRelStr of S opp & xi = xi~ & xy = xy~
           by A1,Th12,LATTICE3:def 6;
          then xi~ >= xy~ by A12,YELLOW_0:60;
          then xi <= xy by LATTICE3:9;
then A13:       f.xi <= x by A11,WAYBEL_1:def 2;
            N.i = (the mapping of N).i by WAYBEL_0:def 8
             .= f.((id X).i) by A1,A2,FUNCT_2:21
             .= f.xi by A1,A2,FUNCT_1:35;
          then f.xi in up(j) by A12;
          then f.xi >= infy(j) by A9,YELLOW_4:2;
         hence thesis by A13,ORDERS_1:26;
        end;
       then infy(j) <= inf (f.:X) by A9,YELLOW_0:31;
      hence thesis by A10,ORDERS_1:25;
     end;
A14:  ex j being Element of N st P[j];
      {infy(j) where j is Element of N: P[j]} =
    {G(j) where j is Element of N: P[j]}
      from FraenkelF'R(A3)
      .= {inf (f.:X) where j is Element of N: P[j]}
      .= {inf (f.:X)} from SingleFraenkel(A14);
   hence lim_inf N = sup {inf (f.:X)} by WAYBEL11:def 6
                  .= inf (f.:X) by YELLOW_0:39;
  end;

theorem Th30:
 for S,T being non empty TopPoset
 for X being non empty filtered Subset of S
 for f being monotone map of S,T
 for Y being 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 map 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 &
    the mapping of N = f*the mapping of X opp+id by WAYBEL_9:def 8;
A3:  the carrier of M = Y &
    M is full SubRelStr of T opp &
    the mapping of M = id Y by WAYBEL19:27,YELLOW_9:7;
A4:  the carrier of X opp+id = X & X opp+id is full SubRelStr of S opp &
    the mapping of X opp+id = id X by WAYBEL19:27,YELLOW_9:7;
then A5: the mapping of N = f|X & the carrier of T <> {} by A2,RELAT_1:94;
then A6: rng the mapping of N = f.:X & dom the mapping of N = X
     by A2,A4,FUNCT_2:def 1,RELAT_1:148;
    then the mapping of N is Function of the carrier of N, Y
     by A1,A2,A4,FUNCT_2:def 1,RELSET_1:11;
   then reconsider g = f|X as map of N,M by A3,A5;
   take g;
   thus the mapping of N = (the mapping of M)*g by A1,A3,A5,A6,RELAT_1:79;
   let m be Element of M;
   consider n being set such that
A7:  n in the carrier of S & n in X & m = f.n by A1,A3,FUNCT_2:115;
   reconsider n as Element of N by A2,A4,A7;
   take n; let p be Element of N;
      p in X by A2,A4;
   then reconsider n' = n, p' = p as Element of S by A7;
      f.p' in the carrier of M by A1,A2,A3,A4,FUNCT_2:43;
   then reconsider fp = f.p' as Element of M;
      X opp+id is SubRelStr of S opp by YELLOW_9:7;
then A8:  N is SubRelStr of S opp & n'~ = n' & p'~ = p' by A2,Th12,LATTICE3:def
6;
A9:  M is full SubRelStr of T opp by YELLOW_9:7;
   assume n <= p;
    then n'~ <= p'~ by A8,YELLOW_0:60;
    then n' >= p' by LATTICE3:9;
    then f.n' >= f.p' by WAYBEL_1:def 2;
    then (f.n')~ <= (f.p')~ & (f.n')~ = m & (f.p')~ = fp &
     the carrier of M <> {} by A7,LATTICE3:9,def 6;
    then fp >= m by A9,YELLOW_0:61;
   hence m <= g.p by A2,A4,FUNCT_1:72;
  end;

theorem
   for S,T being non empty TopPoset
 for X being non empty filtered Subset of S
 for f being monotone map of S,T
 for Y being 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 map 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:41;
  end;

theorem Th32:
 for S being non empty reflexive RelStr, D being 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;
      dom id D = D & rng id D = D by RELAT_1:71;
   then reconsider g = id D as Function of D, the carrier of S
     by FUNCT_2:def 1,RELSET_1:11;
      (id the carrier of S)|D = id D by FUNCT_3:1;
then A1:  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 WELLORD1:15;
   hence thesis by A1,YELLOW_0:def 13,def 14;
  end;

theorem Th33:
 for S,T being up-complete (non empty Poset)
 for f being monotone map of S,T
 for D being 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 map 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 is Element of N: i >= $1};
   deffunc infy(Element of N) = "/\"(up($1), T);
   set NT = {infy(j) where j is Element of N:
             not contradiction};
A1: the RelStr of N = the RelStr of M &
    the mapping of N = f*the mapping of M by WAYBEL_9:def 8;
A2: the carrier of M = X & the mapping of M = id X by Th32;
A3: now let i be Element of N;
     thus N.i = (the mapping of N).i by WAYBEL_0:def 8
             .= f.((id X).i) by A1,A2,FUNCT_2:21
             .= f.i by A1,A2,FUNCT_1:35;
    end;
A4: for i being Element of N holds infy(i) = f.i
     proof let i be Element of N;
         i in X by A1,A2;
      then reconsider x = i as Element of S;
A5:    i <= i;
         N.i = f.x by A3;
       then f.x in up(i) by A5;
then A6:    for z being Element of T st z is_<=_than up(i) holds z <= f.x
        by LATTICE3:def 8;
         f.x is_<=_than up(i)
        proof let z be Element of T; assume z in up(i);
         then consider j being Element of N such that
A7:       z = N.j & j >= i;
         reconsider j as Element of N;
            j in X by A1,A2;
         then reconsider y = j as Element of S;
            M is full SubRelStr of S & the RelStr of S = the RelStr of S
           by Th32;
          then N is full SubRelStr of S by A1,Th12;
          then y >= x by A7,YELLOW_0:60;
          then f.y >= f.x by WAYBEL_1:def 2;
         hence thesis by A3,A7;
        end;
      hence "/\"(up(i), T) = f.i by A6,YELLOW_0:31;
     end;
      NT = f.:X
     proof
      thus NT c= f.:X
       proof let x be set; assume x in NT;
        then consider j being Element of N such that
A8:      x = infy(j);
        reconsider j as Element of N;
           x = f.j & j in X & the carrier of T <> {} by A1,A2,A4,A8;
        hence thesis by FUNCT_2:43;
       end;
      let y be set; assume y in f.:X;
      then consider x being set such that
A9:    x in the carrier of S & x in X & y = f.x by FUNCT_2:115;
      reconsider x as Element of S by A9;
      reconsider i = x as Element of N by A1,A2,A9;
         f.x = infy(i) by A4;
      hence thesis by A9;
     end;
   hence lim_inf N = sup (f.:X) by WAYBEL11:def 6;
  end;

theorem Th34:
 for S being non empty reflexive RelStr
 for D being non empty directed Subset of S
 for i,j being 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;
      dom id D = D & rng id D = D by RELAT_1:71;
   then reconsider g = id D as Function of D, the carrier of S
     by FUNCT_2:def 1,RELSET_1:11;
      (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 Th35:
 for T being Lawson (complete TopLattice)
 for D being 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 & the carrier of N = D by Th32;
   consider K being prebasis of T;
      now let A be Subset of T; assume
A2:   sup D in A;
A3:   K c= the topology of T by CANTOR_1:def 5;
     assume A in K; then A is open by A3,PRE_TOPC:def 5;
      then A has_the_property_(S) by WAYBEL19:36;
     then consider y being Element of T such that
A4:   y in D and
A5:   for x being Element of T st x in D & x >= y holds x in A
       by A2,WAYBEL11:def 3;
     reconsider i = y as Element of N by A1,A4;
     thus N is_eventually_in A
      proof take i; let j be Element of N;
          N.j = (the mapping of N).j & N.i = (the mapping of N).i
         by WAYBEL_0:def 8;
then A6:     j = N.j & y = N.i by A1,FUNCT_1:34;
       assume j >= i;
        then N.j >= N.i by Th34;
       hence thesis by A1,A5,A6;
      end;
    end;
   hence sup D in Lim N 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 such that
A1:      M is subnet of N;
 mode Embedding of M,N -> map of M,N means:
Def3:
  the mapping of M = (the mapping of N)*it &
  for m being Element of N ex n being Element of M st
   for p being Element of M st n <= p holds m <= it.p;
 existence by A1,YELLOW_6:def 12;
end;

theorem Th36:
 for T being non empty 1-sorted
 for N being net of T, M being non empty subnet of N
 for e being Embedding of M,N, i being 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 non empty 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 M.i = ((the mapping of N)*e).i by WAYBEL_0:def 8
      .= (the mapping of N).(e.i) by FUNCT_2:21
      .= N.(e.i) by WAYBEL_0:def 8;
  end;

theorem Th37:
 for T being complete LATTICE
 for N being net of T, M being 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) = {"/\"
({$1.i where i is Element of $1:
    i >= j}, T) where j is Element of $1: not contradiction};
A1:  "\/"(infy(M), T) is_>=_than infy(N)
     proof let t be Element of T; assume t in infy(N);
      then consider j being Element of N such that
A2:    t = "/\"({N.i where i is Element of N: i >= j}, T);
      consider e being Embedding of M,N;
      reconsider j as Element of N;
      consider j' being Element of M such that
A3:    for p being Element of M st j' <= p holds j <= e.p by Def3;
      set X = {N.i where i is Element of N: i >= j};
      set Y = {M.i where i is Element of M: i >= j'};
A4:    ex_inf_of X, T & ex_inf_of Y, T by YELLOW_0:17;
         Y c= X
        proof let y be set; assume y in Y;
         then consider i being Element of M such that
A5:       y = M.i & i >= j';
         reconsider i as Element of M;
            e.i >= j by A3,A5;
          then N.(e.i) in X;
         hence thesis by A5,Th36;
        end;
then A6:    t <= "/\"(Y, T) by A2,A4,YELLOW_0:35;
         "/\"(Y, T) in infy(M);
       then "/\"(Y, T) <= "\/"(infy(M), T) by YELLOW_2:24;
      hence thesis by A6,YELLOW_0:def 2;
     end;
      lim_inf M = "\/"(infy(M), T) & lim_inf N = "\/"(infy(N), T)
     by WAYBEL11:def 6;
   hence thesis by A1,YELLOW_0:32;
  end;

theorem Th38:
 for T being complete LATTICE
 for N being net of T, M being subnet of N
 for e being Embedding of M, N
  st for i being Element of N, j being Element of M st e.j <= i
       ex j' being Element of M st j' >= j & N.i >= M.j'
  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 being Element of N, j being Element of M st e.j <= i
     ex j' being Element of M st j' >= j & N.i >= M.j';
   deffunc infy(net of T) = {"/\"
({$1.i where i is Element of $1:
    i >= j}, T) where j is Element of $1: not contradiction};
      "\/"(infy(N), T) is_>=_than infy(M)
     proof let t be Element of T; assume t in infy(M);
      then consider j being Element of M such that
A2:     t = "/\"({M.i where i is Element of M: i >= j}, T);
      reconsider j as Element of M;
      set j' = e.j;
      set X = {N.i where i is Element of N: i >= j'};
      set Y = {M.i where i is Element of M: i >= j};
         t is_<=_than X
        proof let x be Element of T; assume x in X;
         then consider i being Element of N such that
A3:        x = N.i & i >= j';
         reconsider i as Element of N;
         consider k being Element of M such that
A4:        k >= j & N.i >= M.k by A1,A3;
            M.k in Y by A4;
          then M.k >= t by A2,YELLOW_2:24;
         hence thesis by A3,A4,YELLOW_0:def 2;
        end;
then A5:     t <= "/\"(X, T) by YELLOW_0:33;
         "/\"(X, T) in infy(N);
       then "/\"(X, T) <= "\/"(infy(N), T) by YELLOW_2:24;
      hence t <= "\/"(infy(N), T) by A5,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 lim_inf N >= lim_inf M & lim_inf M >= lim_inf N by Th37,WAYBEL11:def 6
;
   hence thesis by YELLOW_0:def 3;
  end;

theorem
   for T being non empty RelStr
 for N being net of T, M being non empty full SubNetStr of N
  st for i being Element of N
      ex j being 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 being Element of N
     ex j being 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 &
    M is full SubRelStr of N by YELLOW_6:def 8,def 9;
then A3:  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 A2,YELLOW_0:59;
      consider k being Element of N such that
A4:     k >= i & k >= j by YELLOW_6:def 5;
      consider l being Element of N such that
A5:     l >= k & l in the carrier of M by A1;
      reconsider z = l as Element of M by A5;
      take z;
         l >= i & l >= j by A4,A5,YELLOW_0:def 2;
      hence thesis by YELLOW_6:21;
     end;
   then reconsider K = M as net of T by A2;
A6:  now set f = incl(K,N);
A7:    f = id the carrier of K by A3,YELLOW_9:def 1;
     hence the mapping of K = (the mapping of N)*f by A2,RELAT_1:94;
     let m be Element of N;
     consider j being Element of N such that
A8:    j >= m & j in the carrier of K by A1;
     reconsider n = j as Element of K by A8;
     take n; let p be Element of K;
     reconsider q = p as Element of N by A2,YELLOW_0:59;
     assume n <= p; then j <= q & f.p = q by A7,FUNCT_1:35,YELLOW_6:20;
     hence m <= f.p by A8,YELLOW_0:def 2;
    end;
   hence M is subnet of N by YELLOW_6:def 12;
   hence thesis by A6,Def3;
  end;

theorem Th40:
 for T being non empty RelStr, N being net of T
 for i being 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 9;
      the carrier of N|i c= the carrier of N by WAYBEL_9:13;
then A2:  incl(N|i,N) = id the carrier of N|i by 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:94;
   let m be Element of N;
   consider n' being Element of N such that
A3:  n' >= i & n' >= m by YELLOW_6:def 5;
      n' in the carrier of M by A3,WAYBEL_9:def 7;
   then reconsider n = n' as Element of M;
   take n;
   let p be Element of M; reconsider p' = p as Element of N by A1,YELLOW_0:59;
   assume n <= p; then n' <= p' by A1,YELLOW_0:60;
    then m <= p' by A3,YELLOW_0:def 2;
   hence m <= f.p by A2,FUNCT_1:35;
  end;

theorem Th41:
 for T being complete LATTICE, N being net of T
 for i being 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 9;
      the carrier of M c= the carrier of N by WAYBEL_9:13;
then A2:  incl(M,N) = id the carrier of M by YELLOW_9:def 1;
      now let k be Element of N, j be Element of M;
     consider j' being Element of N such that
A3:    j' = j & j' >= i by WAYBEL_9:def 7;
     assume e.j <= k;
then A4:    k >= j' by A2,A3,FUNCT_1:35;
      then k >= i by A3,YELLOW_0:def 2;
then     k in the carrier of M by WAYBEL_9:def 7;
     then reconsider k' = k as Element of M;
     take k'; thus k' >= j by A1,A3,A4,YELLOW_0:61;
        M.k' = N.(e.k') & M.k' <= M.k' by Th36;
     hence N.k >= M.k' by A2,FUNCT_1:35;
    end;
   hence lim_inf (N|i) = lim_inf N by Th38;
  end;

theorem Th42:
 for T being non empty RelStr, N being net of T, X being set
  st N is_eventually_in X
 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 i' being Element of N such that
A1:  for j being Element of N st j >= i' holds N.j in X;
      [#]N is directed & [#]
N = the carrier of N by PRE_TOPC:12,WAYBEL_0:def 6;
   then consider i being Element of N such that
A2: i in [#]N & i' <= i & i' <= i by WAYBEL_0:def 1;
   take i; thus N.i in X by A1,A2;
   let x be set; assume x in rng the mapping of N|i;
   then consider j being set such that
A3:  j in dom the mapping of N|i & x = (the mapping of N|i).j by FUNCT_1:def 5;
A4:  dom the mapping of N|i = the carrier of N|i by FUNCT_2:def 1;
   then reconsider j as Element of N|i by A3;
      the carrier of N|i = {y where y is Element of N: i <= y}
     by WAYBEL_9:12;
   then consider k being Element of N such that
A5:  j = k & i <= k by A3,A4;
A6:  i' <= k by A2,A5,ORDERS_1:26;
      x = (N|i).j by A3,WAYBEL_0:def 8 .= N.k by A5,WAYBEL_9:16;
   hence thesis by A1,A6;
  end;

theorem Th43:  :: see WAYBEL_2:18, for eventually-directed
 for T being Lawson (complete TopLattice)
 for N being 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 being set such that
A1:    i1 in dom the mapping of N & x = (the mapping of N).i1 by FUNCT_1:def 5;
      assume y in F;
      then consider i2 being set such that
A2:    i2 in dom the mapping of N & y = (the mapping of N).i2 by FUNCT_1:def 5;
A3:    dom the mapping of N = the carrier of N by FUNCT_2:def 1;
      then reconsider i1, i2 as Element of N by A1,A2;
      consider j1 being Element of N such that
A4:    for k being Element of N st j1 <= k holds N.i1 >= N.k by WAYBEL_0:12;
      consider j2 being Element of N such that
A5:    for k being Element of N st j2 <= k holds N.i2 >= N.k by WAYBEL_0:12;
      consider j being Element of N such that
A6:    j2 <= j & j1 <= j by YELLOW_6:def 5;
      take z = N.j; z = (the mapping of N).j by WAYBEL_0:def 8;
      hence z in F by A3,FUNCT_1:def 5;
         x = N.i1 & y = N.i2 by A1,A2,WAYBEL_0:def 8;
      hence thesis by A4,A5,A6;
     end;
   hence thesis;
  end;

theorem Th44:
:: 1.7. LEMMA, -- WAYBEL19:44 revised
 for T being Lawson (complete TopLattice)
 for N being eventually-filtered net of T
  holds Lim N = {inf N}
  proof let T be Lawson (complete TopLattice);
   consider S being 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;
A5: now let i be Element of N;
        N.i = (the mapping of N).i by WAYBEL_0:def 8;
     hence N.i in F by A4,FUNCT_1:def 5;
    end;
   thus Lim N c= {inf N}
     proof let p be set; assume
A6:    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 being set such that
A7:       i in dom the mapping of N & u = (the mapping of N).i by FUNCT_1:def 5
;
         reconsider i as Element of N by A4,A7;
         consider ii being Element of N such that
A8:       for k being 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:52;
            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;
             then N.j <= u by A7,WAYBEL_0:def 8;
            hence thesis by WAYBEL_0:17;
           end;
          then Lim N c= downarrow u by A9,WAYBEL19:26;
         hence thesis by A6,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:52;
then A12:    Cl F c= uparrow inf N by A11,PRE_TOPC:49;
         p in Cl F by A6,WAYBEL_9:24;
       then p >= inf N by A12,WAYBEL_0:18;
       then p = inf N by A10,ORDERS_1:25;
      hence thesis by TARSKI:def 1;
     end;
   reconsider K = (sigma T) \/
     {(uparrow x)` where x is Element of T: not contradiction} as prebasis of T
       by WAYBEL19:30;
      now let A be Subset of T; assume
A13:   inf F in A & A in K;
     per cases by A13,XBOOLE_0:def 2;
     suppose
A14:    A in sigma T;
      then reconsider a = A as Subset of S by A1;
         a is open by A1,A14,PRE_TOPC:def 5;
       then a is upper by WAYBEL11:def 4;
then A15:    A is upper by A2,WAYBEL_0:25;
      consider i being Element of N;
      thus N is_eventually_in A
        proof take i; let j be Element of N;
            N.j in F by A5;
          then N.j >= inf F by YELLOW_2:24;
         hence thesis by A13,A15,WAYBEL_0:def 20;
        end;
     suppose A in {(uparrow x)` where x is Element of T: not contradiction};
      then consider x being Element of T such that
A16:    A = (uparrow x)`;
         not inf F >= x by A13,A16,YELLOW_9:1;
       then not F is_>=_than x by YELLOW_0:33;
      then consider y being Element of T such that
A17:    y in F & not y >= x by LATTICE3:def 8;
      consider i being set such that
A18:    i in the carrier of N & y = (the mapping of N).i by A4,A17,FUNCT_1:def
5;
      thus N is_eventually_in A
       proof
        reconsider i as Element of N by A18;
        consider ii being Element of N such that
A19:      for k being 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 & N.i = y by A18,A19,WAYBEL_0:def 8;
         then not N.j >= x by A17,ORDERS_1:26;
        hence N.j in A by A16,YELLOW_9:1;
       end;
    end;
    then inf F in Lim N by WAYBEL19:25;
   hence thesis by A3,ZFMISC_1:37;
  end;

begin :: Lawson topology revisited

theorem Th45:
:: 1.8. THEOREM, (1) <=> (2), generalized, p. 145
 for S,T being Lawson (complete TopLattice)
 for f being meet-preserving map of S,T holds
   f is continuous iff f is directed-sups-preserving &
     for X being non empty Subset of S holds f preserves_inf_of X
  proof let S,T be Lawson (complete TopLattice);
   consider Ss being Scott TopAugmentation of S,
            Ts being Scott TopAugmentation of T,
            Sl being lower correct TopAugmentation of S,
            Tl being lower correct TopAugmentation of T;
      S is TopAugmentation of S & T is TopAugmentation of T by YELLOW_9:44;
then A1:  S is Refinement of Ss,Sl & T is Refinement of Ts,Tl by WAYBEL19:29;
A2: T is TopAugmentation of Ts & S is TopAugmentation of Ss by YELLOW_9:45;
A3:  the RelStr of Ss = the RelStr of S & the RelStr of Sl = the RelStr of S &
    the RelStr of Ts = the RelStr of T & the RelStr of Tl = the RelStr of T
     by YELLOW_9:def 4;
   let f be meet-preserving map of S,T;
   reconsider g = f as map of Sl,Tl by A3;
   reconsider h = f as map of Ss,Ts by A3;
   hereby assume
A4:  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 A3;
      assume
A5:    P is open;
       then C is open by A2,WAYBEL19:37;
then A6:    f"C is open by A4,TOPS_2:55;
         A is upper & h is monotone by A3,A5,WAYBEL11:def 4,WAYBEL_9:1;
       then h"A is upper by WAYBEL17:2;
       then f"C is upper by A3,WAYBEL_0:25;
      hence h"P is open by A2,A6,WAYBEL19:41;
     end;
     then h is continuous by TOPS_2:55;
     then h is directed-sups-preserving by WAYBEL17:22;
    hence f is directed-sups-preserving by A3,Th6;
       for X being 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 f.:{inf F} c= Lim (f*(F opp+id)) &
        f is Function of the carrier of S, the carrier of T by A4,Th24;
        then {f.inf F} c= Lim (f*(F opp+id)) by SETWISEO:13;
then A7:     f.inf F in Lim (f*(F opp+id)) by ZFMISC_1:37;
       reconsider G = f.:F as filtered non empty Subset of T by WAYBEL20:25;
A8:     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:94
         .= G by RELAT_1:148;
          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 A8,YELLOW_2:def 6;
       hence thesis by A7,TARSKI:def 1;
      end;
    hence for X being non empty Subset of S holds f preserves_inf_of X
      by Th4;
   end;
   assume f is directed-sups-preserving;
    then h is directed-sups-preserving by A3,Th6;
then A9:  h is continuous by WAYBEL17:22;
   assume
A10:  for X being non empty Subset of S holds f preserves_inf_of X;
      now let X be non empty Subset of Sl;
     reconsider Y = X as non empty Subset of S by A3;
        f preserves_inf_of Y by A10;
     hence g preserves_inf_of X by A3,WAYBEL_0:65;
    end;
    then g is continuous by WAYBEL19:8;
   hence thesis by A1,A9,WAYBEL19:24;
  end;

theorem Th46:
:: 1.8. THEOREM, (1) <=> (2), p. 145
 for S,T being Lawson (complete TopLattice)
 for f being 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 being finite Subset of S holds f preserves_inf_of X by Def1;
       for X being 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 being non empty Subset of S holds f preserves_inf_of X
     by WAYBEL_0:def 32;
   hence thesis by Th45;
  end;

definition
 let S,T be non empty RelStr;
 let f be map of S,T;
 attr f is lim_infs-preserving means
     for N being net of S holds f.lim_inf N = lim_inf (f*N);
end;

theorem
:: 1.8. THEOREM, (1) <=> (3), p. 145
   for S,T being Lawson (complete TopLattice)
 for f being 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 = {"/\"({M.i where i is Element of M:i >= j},T)
             where j is Element of M: not contradiction};
     reconsider X = {"/\"
({N.i where i is Element of N:i >= j},S)
             where j is Element of N: not contradiction}
       as directed non empty Subset of S by Th25;
A2:    ex_sup_of X,S & f preserves_sup_of X by A1,WAYBEL_0:def 37,YELLOW_0:17;
A3:    the mapping of f*N = f*the mapping of N &
      the RelStr of f*N = the RelStr of N by WAYBEL_9:def 8;
A4:    the carrier of S c= dom f by FUNCT_2:def 1;
     deffunc A(Element of N)
      = {N.i where i is Element of N: i >= $1};
     deffunc INF(Element of N) = "/\"(A($1),S);
     defpred P[set] means not contradiction;
A5:    f.:{INF(i) where i is Element of N: P[i]}
       = {f.INF(i) where i is Element of N: P[i]}
        from FuncFraenkel(A4);
A6:    f.:X = Y
       proof
A7:      now let j be Element of N;
          let j' be Element of M such that
A8:        j' = j;
          defpred Q[Element of N] means $1 >= j;
          defpred Q'[Element of M] means $1 >= j';
          deffunc F(Element of N) = f.(N.$1);
          deffunc G(set) = f.((the mapping of N).$1);
A9:        for v being Element of N st Q[v]
            holds F(v) = G(v) by WAYBEL_0:def 8;
          deffunc H(set) = (f*the mapping of N).$1;
          deffunc I(Element of M) = M.$1;
A10:        for v being Element of N st Q[v] holds G(v) = H(v)
             by FUNCT_2:21;
A11:        for v being Element of M st Q'[v] holds H(v) = I(v)
             by A3,WAYBEL_0:def 8;
          defpred P[set] means [j',$1] in the InternalRel of N;
A12:        for v being Element of N
            holds Q[v] iff P[v] by A8,ORDERS_1:def 9;
A13:        for v being Element of M holds P[v] iff Q'[v]
             by A3,ORDERS_1:def 9;
          deffunc N(Element of N) = N.$1;
          thus f.:A(j)
            = f.:{N(i) where i is Element of N: Q[i]}
           .= {f.(N(k)) where k is Element of N: Q[k]}
             from FuncFraenkel(A4)
           .= {F(k) where k is Element of N: Q[k]}
           .= {G(s) where s is Element of N: Q[s]}
             from FraenkelF'R(A9)
           .= {H(o) where o is Element of N: Q[o]}
             from FraenkelF'R(A10)
           .= {H(r) where r is Element of N: P[r]}
             from Fraenkel6'(A12)
           .= {H(m) where m is Element of M: P[m]} by A3
           .= {H(q) where q is Element of M: Q'[q]}
             from Fraenkel6'(A13)
           .= {I(n) where n is Element of M: Q'[n]}
             from FraenkelF'R(A11)
           .= {M.n where n is Element of M: n >= j'};
         end;
A14:     now let j be Element of N;
             A(j) c= the carrier of S
            proof let b be set; assume b in A(j);
              then ex i being Element of N st b = N.i & i >= j;
             hence thesis;
            end;
          then reconsider A = A(j) as Subset of S;
             f preserves_inf_of A & ex_inf_of A,S
            by A1,WAYBEL_0:def 32,YELLOW_0:17;
          hence f."/\"(A(j),S) = "/\"(f.:A(j), T) by WAYBEL_0:def 30;
         end;
        thus f.:X c= Y
         proof let a be set; assume a in f.:X;
          then consider j being Element of N such that
A15:        a = f."/\"
({N.i where i is Element of N:i >= j},S) by A5;
A16:        a = "/\"(f.:A(j),T) by A14,A15;
          reconsider j' = j as Element of M by A3;
             f.:A(j) = {M.n where n is Element of M: n >=
 j'} by A7;
          hence thesis by A16;
         end;
        let a be set; assume a in Y;
        then consider j' being Element of M such that
A17:      a = "/\"({M.n where n is Element of M: n >= j'},T);
        reconsider j = j' as Element of N by A3;
           a = "/\"(f.:A(j),T) by A7,A17 .= f."/\"(A(j),S) by A14;
        hence thesis by A5;
       end;
     thus f.lim_inf N = f.sup X by WAYBEL11:def 6
      .= sup (f.:X) by A2,WAYBEL_0:def 31
      .= lim_inf (f*N) by A6,WAYBEL11:def 6;
    end;
   assume
A18:  for N being net of S holds f.lim_inf N = lim_inf (f*N);
A19:  f is directed-sups-preserving
     proof let D be Subset of S; assume D is non empty directed;
      then reconsider D' = 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 D' by WAYBEL17:10
           .= lim_inf (f*Net-Str D') by A18
           .= sup (f.:D) by Th33;
     end;
A20:  for X being 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:25;
     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 A18
               .= inf fX by Th29
               .= lim_inf (fX opp+id) by Th28;
       hence thesis by Th28;
      end;
    end;
    then f is infs-preserving by A20,WAYBEL_0:71;
   hence f is continuous by A19,Th46;
  end;

theorem Th48:
:: 1.11. THEOREM, (1) => (2a), p. 147
 for T being Lawson (complete continuous TopLattice)
 for S being meet-inheriting full non empty SubRelStr of T
  st Top T in the carrier of S &
     ex X being 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 being 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 rng the mapping of N = Y by RELAT_1:71;
then A4:      N is_eventually_in X by A2,Th27;
          Lim N = {inf F} by WAYBEL19:43;
        then {inf F} c= Cl X by A4,WAYBEL19:26;
        then {inf F} c= X by A3,PRE_TOPC:52;
       hence "/\"(Y, T) in the carrier of S by A2,ZFMISC_1:37;
      end;
    hence S is infs-inheriting by A1,Th16;
   end;

theorem Th49:
:: 1.11. THEOREM, (1) => (2b), p. 147
 for T being Lawson (complete continuous TopLattice)
 for S being full non empty SubRelStr of T
  st ex X being 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 being 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 & the carrier of N = D by Th32;
     then rng the mapping of N = Y by RELAT_1:71;
     then N is_eventually_in X by A1,Th27;
     then Lim N c= Cl X by WAYBEL19:26;
then A3:   Lim N c= X by A2,PRE_TOPC:52;
       sup D in Lim N by Th35;
    hence "\/"(Y,T) in the carrier of S by A1,A3;
   end;

theorem Th50:
:: 1.11. THEOREM, (2) => (1), p. 147
 for T being Lawson (complete continuous TopLattice)
 for S being infs-inheriting directed-sups-inheriting full non empty
             SubRelStr of T
 ex X being 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;
      the carrier of S c= the carrier of T by YELLOW_0:def 13;
   then reconsider X = the carrier of S as Subset of T;
   take X; thus X = the carrier of S;
   reconsider S as complete CLSubFrame of T by Th18;
   consider SL being Lawson correct TopAugmentation of S;
A1:  the RelStr of SL = the RelStr of S by YELLOW_9:def 4;
then A2: [#]SL = X by PRE_TOPC:12;
   set f = incl(SL,T), f' = incl(S,T);
      the carrier of S c= the carrier of T by YELLOW_0:def 13;
then A3: f = id the carrier of SL & f' = id the carrier of SL
     by A1,YELLOW_9:def 1;
A4:  [#]SL is compact by COMPTS_1:10;
      f' is infs-preserving & f' is directed-sups-preserving &
    the RelStr of T = the RelStr of T by Th8,Th10;
then A5:  f is infs-preserving directed-sups-preserving by A1,A3,Th6;
    then f is SemilatticeHomomorphism of SL,T by Th5;
    then f is continuous by A5,Th46;
    then f.:[#]SL is compact by A4,WEIERSTR:14;
    then X is compact by A2,A3,BORSUK_1:3;
   hence X is closed by COMPTS_1:16;
  end;

theorem Th51:
:: 1.11. THEOREM, (2) => (3+), p. 147
 for T being Lawson (complete continuous TopLattice)
 for S being infs-inheriting directed-sups-inheriting full non empty
             SubRelStr of T
 for N being 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 being Element of N such that
A1: N.a in X & rng the mapping of N|a c= X by Th42;
   deffunc up(Element of N|a) =
      {N|a.i where i is Element of N|a: i >= $1};
   reconsider iN = {"/\"(up(j), T)
      where j is Element of N|a: not contradiction}
    as directed non empty Subset of T by Th25;
      iN c= X
     proof let z be set; assume z in iN;
      then consider j being Element of N|a such that
A2:    z = "/\"(up(j), T);
         up(j) c= X
        proof let u be set; assume u in up(j);
         then consider i being Element of N|a such that
A3:       u = (N|a).i & i >= j;
            u = (the mapping of N|a).i & the carrier of N|a <> {}
           by A3,WAYBEL_0:def 8;
          then u in rng the mapping of N|a by FUNCT_2:6;
         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;
      jN is directed & ex_sup_of jN,T by WAYBEL10:24,YELLOW_0:17;
    then "\/"(jN,T) in the carrier of S by WAYBEL_0:def 4;
    then lim_inf (N|a) in X by WAYBEL11:def 6;
   hence lim_inf N in X by Th41;
  end;

theorem Th52:
:: 1.11. THEOREM, (3) => (2a), p. 147
 for T being Lawson (complete continuous TopLattice)
 for S being meet-inheriting full non empty SubRelStr of T
  st Top T in the carrier of S &
     for N being 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 being 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 by RELAT_1:71;
         lim_inf (F opp+id) = inf F by Th28;
      hence "/\"(Y, T) in the carrier of S by A2,A3;
     end;
   hence S is infs-inheriting by A1,Th16;
  end;

theorem Th53:
:: 1.11. THEOREM, (3) => (2b), p. 147
 for T being Lawson (complete continuous TopLattice)
 for S being full non empty SubRelStr of T
  st for N being 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 being 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 by RELAT_1:71;
      lim_inf Net-Str F = sup F by WAYBEL17:10;
   hence "\/"(Y, T) in the carrier of S by A1,A2;
  end;

theorem
:: 1.11. THEOREM, (1) <=> (3+), p. 147
   for T being Lawson (complete continuous TopLattice)
 for S being meet-inheriting full non empty SubRelStr of T
 for X being Subset of T st X = the carrier of S & Top T in X
  holds
   X is closed iff
    for N being 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 & 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,Th48,Th49;
    hence for N being net of T st N is_eventually_in X holds lim_inf N in X
      by A1,Th51;
   end;
   assume
A2: for N being net of T st N is_eventually_in X holds lim_inf N in X;
      now let N be net of T; assume
        rng the mapping of N c= the carrier of S;
      then N is_eventually_in X by A1,Th27;
     hence lim_inf N in the carrier of S by A1,A2;
    end;
    then S is infs-inheriting directed-sups-inheriting by A1,Th52,Th53;
    then ex X being Subset of T st X = the carrier of S & X is closed
     by Th50;
   hence thesis by A1;
  end;


Back to top