The Mizar article:

Kernel Projections and Quotient Lattices

by
Piotr Rudnicki

Received July 6, 1998

Copyright (c) 1998 Association of Mizar Users

MML identifier: WAYBEL20
[ MML identifier index ]


environ

 vocabulary RELAT_1, FUNCT_5, FUNCT_1, EQREL_1, RELAT_2, ORDERS_1, PRE_TOPC,
      YELLOW_0, BOOLE, LATTICES, LATTICE3, ORDINAL2, WAYBEL_0, QUANTAL1,
      WELLORD1, CAT_1, BHSP_3, WAYBEL_1, GROUP_6, SEQM_3, YELLOW_1, WAYBEL_3,
      PBOOLE, CARD_3, FUNCT_4, FINSET_1, WAYBEL16, WAYBEL_5, BINOP_1, SETFAM_1,
      WAYBEL20, PARTFUN1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, SETFAM_1,
      RELAT_2, FUNCT_1, PARTFUN1, FUNCT_2, FINSET_1, DOMAIN_1, EQREL_1, PBOOLE,
      FUNCT_3, FUNCT_5, FUNCT_7, STRUCT_0, ORDERS_1, LATTICE3, GRCAT_1,
      PRE_TOPC, QUANTAL1, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_3, WAYBEL_0,
      WAYBEL_1, WAYBEL_3, WAYBEL_5, WAYBEL16;
 constructors DOMAIN_1, FUNCT_7, GRCAT_1, QUANTAL1, ORDERS_3, TOPS_2, YELLOW_3,
      WAYBEL_1, WAYBEL16;
 clusters STRUCT_0, FINSET_1, LATTICE3, RELSET_1, YELLOW_0, YELLOW_2, YELLOW_3,
      YELLOW_9, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL10, SUBSET_1, RELAT_1,
      FUNCT_2, PARTFUN1;
 requirements SUBSET, BOOLE;
 definitions TARSKI, RELAT_2, LATTICE3, LATTICE5, YELLOW_0, WAYBEL_0, WAYBEL_1,
      WAYBEL_3;
 theorems TARSKI, ZFMISC_1, RELAT_1, RELSET_1, RELAT_2, FUNCT_1, FUNCT_2,
      FUNCT_3, FUNCT_5, FUNCT_7, CARD_3, PBOOLE, ORDERS_1, LATTICE3, LATTICE5,
      QUANTAL1, GRCAT_1, EQREL_1, EXTENS_1, YELLOW_0, YELLOW_2, YELLOW_3,
      YELLOW10, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_5, WAYBEL_8, WAYBEL13,
      WAYBEL15, WAYBEL16, WAYBEL17, XBOOLE_0, XBOOLE_1, PARTFUN1;
 schemes YELLOW_0, FUNCT_2, PRALG_2;

begin :: Preliminaries

theorem Th1:
 for X being set, S being Subset of id X holds proj1 S = proj2 S
proof let X be set, S be Subset of id X;
    now let x be set;
   hereby assume x in proj1 S; then consider y being set such that
 A1: [x, y] in S by FUNCT_5:def 1;
       x in X & x = y by A1,RELAT_1:def 10;
    hence x in proj2 S by A1,FUNCT_5:def 2;
   end;
   assume x in proj2 S; then consider y being set such that
 A2: [y, x] in S by FUNCT_5:def 2;
       y in X & x = y by A2,RELAT_1:def 10;
    hence x in proj1 S by A2,FUNCT_5:def 1;
  end;
 hence proj1 S = proj2 S by TARSKI:2;
end;

theorem Th2:
 for X, Y being non empty set, f being Function of X, Y
  holds [:f, f:]"(id Y) is Equivalence_Relation of X
proof let X, Y be non empty set, f be Function of X, Y;
  set ff = [:f, f:]"(id Y);
A1: dom [:f, f:] = [:dom f, dom f:] by FUNCT_3:def 9;
A2: dom f = X by FUNCT_2:def 1;
  reconsider R' = ff as Relation of X by RELSET_1:def 1;
    R' is total symmetric transitive proof
     R' is_reflexive_in X
      proof let x be set; assume
    A3: x in X;
       then reconsider x' = x as Element of X;
    A4: [x, x] in dom [:f, f:] by A1,A2,A3,ZFMISC_1:def 2;
    A5: [f.x', f.x'] in id Y by RELAT_1:def 10;
          [f.x, f.x] = [:f, f:].[x,x] by A2,A3,FUNCT_3:def 9;
     hence [x, x] in R' by A4,A5,FUNCT_1:def 13;
    end;
    then
A6:  dom R' = X & field R' = X by ORDERS_1:98;
    hence R' is total by PARTFUN1:def 4;
     R' is_symmetric_in X
     proof let x, y be set; assume
    A7: x in X & y in X & [x,y] in R';
       then reconsider x' = x, y' = y as Element of X;
    A8: [x, y] in dom [:f, f:] & [:f, f:].[x,y] in id Y
           by A7,FUNCT_1:def 13;
    A9: [f.x, f.y] = [:f, f:].[x, y] by A2,A7,FUNCT_3:def 9;
    then A10: f.x' = f.y' by A8,RELAT_1:def 10;
    A11: [y, x] in dom [:f, f:] by A1,A2,A7,ZFMISC_1:def 2;
          [f.y, f.x] = [:f, f:].[y, x] by A2,A7,FUNCT_3:def 9;
     hence [y,x] in R' by A8,A9,A10,A11,FUNCT_1:def 13;
    end;
    hence R' is symmetric by A6,RELAT_2:def 11;
     R' is_transitive_in X
     proof let x, y, z be set such that
    A12:   x in X & y in X & z in X and
    A13:  [x,y] in R' & [y,z] in R';
       reconsider y'=y, z'=z as Element of X by A12;
    A14: [x, y] in dom [:f, f:] & [:f, f:].[x,y] in id Y
                  by A13,FUNCT_1:def 13;
    A15: [y, z] in dom [:f, f:] & [:f, f:].[y, z] in id Y
                  by A13,FUNCT_1:def 13;
    A16: [f.x, f.y] = [:f, f:].[x, y] by A2,A12,FUNCT_3:def 9;
      [f.y, f.z] = [:f, f:].[y, z] by A2,A12,FUNCT_3:def 9;
    then A17: f.y' = f.z' by A15,RELAT_1:def 10;
    A18: [x, z] in dom [:f, f:] by A1,A2,A12,ZFMISC_1:def 2;
            [f.x, f.z] = [:f, f:].[x, z] by A2,A12,FUNCT_3:def 9;
     hence [x,z] in R' by A14,A16,A17,A18,FUNCT_1:def 13;
    end;
   hence R' is transitive by A6,RELAT_2:def 16;
  end;
 hence ff is Equivalence_Relation of X;
end;

definition
 let L1, L2, T1, T2 be RelStr, f be map of L1, T1, g be map of L2, T2;
 redefine func [:f, g:] -> map of [:L1, L2:], [:T1, T2:];
  coherence proof
    the carrier of [:L1, L2:] = [:the carrier of L1, the carrier of L2:] &
  the carrier of [:T1, T2:] = [:the carrier of T1, the carrier of T2:]
     by YELLOW_3:def 2;
  hence [:f, g:] is map of [:L1, L2:], [:T1, T2:];
 end;
end;

theorem Th3:
 for f, g being Function, X being set holds
  proj1 ([:f, g:].:X) c= f.:proj1 X & proj2 ([:f, g:].:X) c= g.:proj2 X
proof let f, g be Function, X be set;
A1: dom [:f, g:] = [:dom f, dom g:] by FUNCT_3:def 9;
  hereby let x be set;
      assume x in proj1 ([:f, g:].:X);
     then consider y being set such that
  A2: [x, y] in [:f, g:].:X by FUNCT_5:def 1;
     consider xy being set such that
  A3: xy in dom [:f, g:] and
  A4: xy in X and
  A5: [x, y] = [:f, g:].xy by A2,FUNCT_1:def 12;
      consider x',y' being set such that
  A6: x' in dom f & y' in dom g & xy = [x',y'] by A1,A3,ZFMISC_1:def 2;
     [x, y] = [f.x', g.y'] by A5,A6,FUNCT_3:def 9;
  then A7: x = f.x' by ZFMISC_1:33;
        x' in proj1 X by A4,A6,FUNCT_5:def 1;
    hence x in f.:proj1 X by A6,A7,FUNCT_1:def 12;
   end;
   let y be set;
      assume y in proj2 ([:f, g:].:X);
     then consider x being set such that
  A8: [x, y] in [:f, g:].:X by FUNCT_5:def 2;
     consider xy being set such that
  A9: xy in dom [:f, g:] and
  A10: xy in X and
  A11: [x, y] = [:f, g:].xy by A8,FUNCT_1:def 12;
      consider x',y' being set such that
  A12: x' in dom f & y' in dom g & xy = [x',y'] by A1,A9,ZFMISC_1:def 2;
     [x, y] = [f.x', g.y'] by A11,A12,FUNCT_3:def 9;
  then A13: y = g.y' by ZFMISC_1:33;
        y' in proj2 X by A10,A12,FUNCT_5:def 2;
    hence y in g.:proj2 X by A12,A13,FUNCT_1:def 12;
end;

theorem Th4:
 for f, g being Function, X being set
  st X c= [:dom f, dom g:]
   holds proj1 ([:f, g:].:X) = f.:proj1 X & proj2 ([:f, g:].:X) = g.:proj2 X
proof let f, g be Function, X be set such that
A1: X c= [:dom f, dom g:];
A2: dom [:f, g:] = [:dom f, dom g:] by FUNCT_3:def 9;
A3: proj1 ([:f, g:].:X) c= f.:proj1 X by Th3;
A4: proj2 ([:f, g:].:X) c= g.:proj2 X by Th3;
    now let x be set;
   thus x in proj1 ([:f, g:].:X) implies x in f.:proj1 X by A3;
   assume x in f.:proj1 X; then consider x' being set such that
  A5: x' in dom f and
  A6: x' in proj1 X and
  A7: x = f.x' by FUNCT_1:def 12;
      consider y' being set such that
  A8: [x', y'] in X by A6,FUNCT_5:def 1;
        y' in dom g by A1,A8,ZFMISC_1:106;
      then [:f, g:].[x', y'] = [f.x', g.y'] by A5,FUNCT_3:def 9;
      then [x, g.y'] in [:f, g:].:X by A1,A2,A7,A8,FUNCT_1:def 12;
   hence x in proj1 ([:f, g:].:X) by FUNCT_5:def 1;
  end;
 hence proj1 ([:f, g:].:X) = f.:proj1 X by TARSKI:2;
    now let x be set;
   thus x in proj2 ([:f, g:].:X) implies x in g.:proj2 X by A4;
   assume x in g.:proj2 X; then consider x' being set such that
  A9: x' in dom g and
  A10: x' in proj2 X and
  A11: x = g.x' by FUNCT_1:def 12;
      consider y' being set such that
  A12: [y', x'] in X by A10,FUNCT_5:def 2;
        y' in dom f by A1,A12,ZFMISC_1:106;
      then [:f, g:].[y', x'] = [f.y', g.x'] by A9,FUNCT_3:def 9;
      then [f.y', x] in [:f, g:].:X by A1,A2,A11,A12,FUNCT_1:def 12;
   hence x in proj2 ([:f, g:].:X) by FUNCT_5:def 2;
  end;
 hence proj2 ([:f, g:].:X) = g.:proj2 X by TARSKI:2;
end;

theorem Th5: :: Grzesiek
 for S being non empty antisymmetric RelStr st ex_inf_of {},S
  holds S is upper-bounded
  proof let S be non empty antisymmetric RelStr; assume
A1:  ex_inf_of {},S;
   take Top S; let x be Element of S;
      {} is_>=_than x & "/\"({},S) = Top S by YELLOW_0:6,def 12;
   hence thesis by A1,YELLOW_0:31;
  end;

theorem Th6:
 for S being non empty antisymmetric RelStr st ex_sup_of {},S
  holds S is lower-bounded
 proof let S be non empty antisymmetric RelStr; assume
A1:  ex_sup_of {},S;
   take Bottom S; let x be Element of S;
      {} is_<=_than x & "\/"({},S) = Bottom S by YELLOW_0:6,def 11;
   hence thesis by A1,YELLOW_0:30;
  end;

theorem Th7: :: generealized YELLOW_3:47, YELLOW10:6
for L1,L2 being antisymmetric (non empty RelStr), D being Subset of [:L1,L2:]
  st ex_inf_of D,[:L1,L2:] holds inf D = [inf proj1 D,inf proj2 D]
proof let L1,L2 be antisymmetric (non empty RelStr), D be Subset of [:L1,L2:]
 such that
A1: ex_inf_of D,[:L1,L2:];
 per cases;
 suppose D <> {};
  hence inf D = [inf proj1 D,inf proj2 D] by A1,YELLOW_3:47;
 suppose D = {};
   then ex_inf_of {},L1 & ex_inf_of {},L2 by A1,FUNCT_5:10,YELLOW_3:42;
   then L1 is upper-bounded & L2 is upper-bounded by Th5;
  hence inf D = [inf proj1 D,inf proj2 D] by A1,YELLOW10:6;
end;

theorem Th8: :: generealized YELLOW_3:46, YELLOW10:5
for L1,L2 being antisymmetric (non empty RelStr), D being Subset of [:L1,L2:]
 st ex_sup_of D,[:L1,L2:] holds sup D = [sup proj1 D,sup proj2 D]
proof let L1,L2 be antisymmetric (non empty RelStr), D be Subset of [:L1,L2:]
 such that
A1: ex_sup_of D,[:L1,L2:];
 per cases;
 suppose D <> {};
  hence sup D = [sup proj1 D,sup proj2 D] by A1,YELLOW_3:46;
 suppose D = {};
   then ex_sup_of {},L1 & ex_sup_of {},L2 by A1,FUNCT_5:10,YELLOW_3:41;
   then L1 is lower-bounded & L2 is lower-bounded by Th6;
  hence sup D = [sup proj1 D,sup proj2 D] by A1,YELLOW10:5;
end;

theorem Th9:
 for L1, L2, T1, T2 being antisymmetric non empty RelStr,
     f being map of L1, T1, g being map of L2, T2
  st f is infs-preserving & g is infs-preserving
   holds [:f, g:] is infs-preserving
proof let L1, L2, T1, T2 be antisymmetric non empty RelStr,
          f be map of L1, T1, g be map of L2, T2 such that
A1: f is infs-preserving & g is infs-preserving;
 let X be Subset of [:L1, L2:];
A2: f preserves_inf_of proj1 X & g preserves_inf_of proj2 X
      by A1,WAYBEL_0:def 32;
 assume
A3: ex_inf_of X, [:L1, L2:];
then A4: ex_inf_of proj1 X, L1 & ex_inf_of proj2 X, L2 by YELLOW_3:42;
  set iX = [:f, g:].:X;
A5: dom f = the carrier of L1 & dom g = the carrier of L2 by FUNCT_2:def 1;
     X c= the carrier of [:L1, L2:];
   then X c= [:the carrier of L1, the carrier of L2:] by YELLOW_3:def 2;
then A6: proj1 iX = f.:proj1 X & proj2 iX = g.:proj2 X by A5,Th4;
  then ex_inf_of proj1 iX, T1 & ex_inf_of proj2 iX, T2 by A2,A4,WAYBEL_0:def 30
;
 hence
      ex_inf_of ([:f, g:].:X), [:T1, T2:] by YELLOW_3:42;
 hence inf ([:f, g:].:X)
    = [inf (f.:proj1 X), inf (g.:proj2 X)] by A6,Th7
   .= [f.inf proj1 X, inf (g.:proj2 X)] by A2,A4,WAYBEL_0:def 30
   .= [f.inf proj1 X, g.inf proj2 X] by A2,A4,WAYBEL_0:def 30
   .= [:f, g:].[inf proj1 X, inf proj2 X] by A5,FUNCT_3:def 9
   .= [:f, g:].inf X by A3,Th7;
end;

theorem
   for L1, L2, T1, T2 being antisymmetric reflexive non empty RelStr,
     f being map of L1, T1, g being map of L2, T2
  st f is filtered-infs-preserving & g is filtered-infs-preserving
   holds [:f, g:] is filtered-infs-preserving
proof let L1, L2, T1, T2 be antisymmetric reflexive non empty RelStr,
          f be map of L1, T1, g be map of L2, T2 such that
A1: f is filtered-infs-preserving & g is filtered-infs-preserving;
 let X be Subset of [:L1, L2:]; assume
   X is non empty filtered;
    then proj1 X is non empty filtered & proj2 X is non empty filtered
     by YELLOW_3:21,24;
then A2: f preserves_inf_of proj1 X & g preserves_inf_of proj2 X
      by A1,WAYBEL_0:def 36;
 assume
A3: ex_inf_of X, [:L1, L2:];
then A4: ex_inf_of proj1 X, L1 & ex_inf_of proj2 X, L2 by YELLOW_3:42;
  set iX = [:f, g:].:X;
A5: dom f = the carrier of L1 & dom g = the carrier of L2 by FUNCT_2:def 1;
     X c= the carrier of [:L1, L2:];
   then X c= [:the carrier of L1, the carrier of L2:] by YELLOW_3:def 2;
then A6: proj1 iX = f.:proj1 X & proj2 iX = g.:proj2 X by A5,Th4;
  then ex_inf_of proj1 iX, T1 & ex_inf_of proj2 iX, T2 by A2,A4,WAYBEL_0:def 30
;
 hence
      ex_inf_of ([:f, g:].:X), [:T1, T2:] by YELLOW_3:42;
 hence inf ([:f, g:].:X)
    = [inf (f.:proj1 X), inf (g.:proj2 X)] by A6,Th7
   .= [f.inf proj1 X, inf (g.:proj2 X)] by A2,A4,WAYBEL_0:def 30
   .= [f.inf proj1 X, g.inf proj2 X] by A2,A4,WAYBEL_0:def 30
   .= [:f, g:].[inf proj1 X, inf proj2 X] by A5,FUNCT_3:def 9
   .= [:f, g:].inf X by A3,Th7;
end;

theorem
   for L1, L2, T1, T2 being antisymmetric non empty RelStr,
     f being map of L1, T1, g being map of L2, T2
  st f is sups-preserving & g is sups-preserving
   holds [:f, g:] is sups-preserving
proof let L1, L2, T1, T2 be antisymmetric non empty RelStr,
          f be map of L1, T1, g be map of L2, T2 such that
A1: f is sups-preserving & g is sups-preserving;
 let X be Subset of [:L1, L2:];
A2: f preserves_sup_of proj1 X & g preserves_sup_of proj2 X
      by A1,WAYBEL_0:def 33;
 assume
A3: ex_sup_of X, [:L1, L2:];
then A4: ex_sup_of proj1 X, L1 & ex_sup_of proj2 X, L2 by YELLOW_3:41;
  set iX = [:f, g:].:X;
A5: dom f = the carrier of L1 & dom g = the carrier of L2 by FUNCT_2:def 1;
     X c= the carrier of [:L1, L2:];
   then X c= [:the carrier of L1, the carrier of L2:] by YELLOW_3:def 2;
then A6: proj1 iX = f.:proj1 X & proj2 iX = g.:proj2 X by A5,Th4;
  then ex_sup_of proj1 iX, T1 & ex_sup_of proj2 iX, T2 by A2,A4,WAYBEL_0:def 31
;
 hence
      ex_sup_of ([:f, g:].:X), [:T1, T2:] by YELLOW_3:41;
 hence sup ([:f, g:].:X)
    = [sup (f.:proj1 X), sup (g.:proj2 X)] by A6,Th8
   .= [f.sup proj1 X, sup (g.:proj2 X)] by A2,A4,WAYBEL_0:def 31
   .= [f.sup proj1 X, g.sup proj2 X] by A2,A4,WAYBEL_0:def 31
   .= [:f, g:].[sup proj1 X, sup proj2 X] by A5,FUNCT_3:def 9
   .= [:f, g:].sup X by A3,Th8;
end;

theorem Th12:
 for L1, L2, T1, T2 being antisymmetric reflexive non empty RelStr,
     f being map of L1, T1, g being map of L2, T2
  st f is directed-sups-preserving & g is directed-sups-preserving
   holds [:f, g:] is directed-sups-preserving
proof let L1, L2, T1, T2 be antisymmetric reflexive non empty RelStr,
          f be map of L1, T1, g be map of L2, T2 such that
A1: f is directed-sups-preserving & g is directed-sups-preserving;
 let X be Subset of [:L1, L2:]; assume
   X is non empty directed;
    then proj1 X is non empty directed & proj2 X is non empty directed
     by YELLOW_3:21,22;
then A2: f preserves_sup_of proj1 X & g preserves_sup_of proj2 X
      by A1,WAYBEL_0:def 37;
 assume
A3: ex_sup_of X, [:L1, L2:];
then A4: ex_sup_of proj1 X, L1 & ex_sup_of proj2 X, L2 by YELLOW_3:41;
  set iX = [:f, g:].:X;
A5: dom f = the carrier of L1 & dom g = the carrier of L2 by FUNCT_2:def 1;
     X c= the carrier of [:L1, L2:];
   then X c= [:the carrier of L1, the carrier of L2:] by YELLOW_3:def 2;
then A6: proj1 iX = f.:proj1 X & proj2 iX = g.:proj2 X by A5,Th4;
  then ex_sup_of proj1 iX, T1 & ex_sup_of proj2 iX, T2 by A2,A4,WAYBEL_0:def 31
;
 hence
      ex_sup_of ([:f, g:].:X), [:T1, T2:] by YELLOW_3:41;
 hence sup ([:f, g:].:X)
    = [sup (f.:proj1 X), sup (g.:proj2 X)] by A6,Th8
   .= [f.sup proj1 X, sup (g.:proj2 X)] by A2,A4,WAYBEL_0:def 31
   .= [f.sup proj1 X, g.sup proj2 X] by A2,A4,WAYBEL_0:def 31
   .= [:f, g:].[sup proj1 X, sup proj2 X] by A5,FUNCT_3:def 9
   .= [:f, g:].sup X by A3,Th8;
end;

theorem Th13:
 for L being antisymmetric non empty RelStr, X being Subset of [:L, L:]
  st X c= id the carrier of L & ex_inf_of X, [:L, L:]
   holds inf X in id the carrier of L
proof let L be antisymmetric non empty RelStr,
          X be Subset of [:L, L:] such that
A1: X c= id the carrier of L and
A2: ex_inf_of X, [:L, L:];
A3: inf X = [inf proj1 X, inf proj2 X] by A2,Th7;
     inf proj1 X = inf proj2 X by A1,Th1;
 hence inf X in id the carrier of L by A3,RELAT_1:def 10;
end;

theorem Th14:
 for L being antisymmetric non empty RelStr, X being Subset of [:L, L:]
  st X c= id the carrier of L & ex_sup_of X, [:L, L:]
   holds sup X in id the carrier of L
proof let L be antisymmetric non empty RelStr,
          X be Subset of [:L, L:] such that
A1: X c= id the carrier of L and
A2: ex_sup_of X, [:L, L:];
A3: sup X = [sup proj1 X, sup proj2 X] by A2,Th8;
     sup proj1 X = sup proj2 X by A1,Th1;
 hence sup X in id the carrier of L by A3,RELAT_1:def 10;
end;

theorem Th15:
 for L, M being non empty RelStr
  st L, M are_isomorphic & L is reflexive holds M is reflexive
proof let L, M be non empty RelStr such that
A1: L, M are_isomorphic and
A2: L is reflexive;
     M, L are_isomorphic by A1,WAYBEL_1:7;
   then consider f being map of M, L such that
A3: f is isomorphic by WAYBEL_1:def 8;
 let x be Element of M;
   reconsider fx = f.x as Element of L;
     fx <= fx by A2,YELLOW_0:def 1;
 hence x <= x by A3,WAYBEL_0:66;
end;

theorem Th16:
 for L, M being non empty RelStr
  st L, M are_isomorphic & L is transitive holds M is transitive
proof let L, M be non empty RelStr such that
A1: L, M are_isomorphic and
A2: L is transitive;
     M, L are_isomorphic by A1,WAYBEL_1:7;
   then consider f being map of M, L such that
A3: f is isomorphic by WAYBEL_1:def 8;
 let x, y, z be Element of M such that
A4: x <= y & y <= z;
   reconsider fx = f.x as Element of L;
   reconsider fy = f.y as Element of L;
   reconsider fz = f.z as Element of L;
     fx <= fy & fy <= fz by A3,A4,WAYBEL_0:66;
   then fx <= fz by A2,YELLOW_0:def 2;
 hence x <= z by A3,WAYBEL_0:66;
end;

theorem Th17:
 for L, M being non empty RelStr
  st L, M are_isomorphic & L is antisymmetric holds M is antisymmetric
proof let L, M be non empty RelStr such that
A1: L, M are_isomorphic and
A2: L is antisymmetric;
     M, L are_isomorphic by A1,WAYBEL_1:7;
   then consider f being map of M, L such that
A3: f is isomorphic by WAYBEL_1:def 8;
A4: f is one-to-one by A3,WAYBEL_0:66;
 let x, y be Element of M such that
A5: x <= y & y <= x;
   reconsider fx = f.x as Element of L;
   reconsider fy = f.y as Element of L;
   A6: dom f = the carrier of M by FUNCT_2:def 1;
     fx <= fy & fy <= fx by A3,A5,WAYBEL_0:66;
   then fx = fy by A2,YELLOW_0:def 3;
 hence x = y by A4,A6,FUNCT_1:def 8;
end;

theorem Th18:  :: stolen from WAYBEL13:30
 for L, M being non empty RelStr
  st L, M are_isomorphic & L is complete holds M is complete
proof let L, M be non empty RelStr such that
A1: L, M are_isomorphic and
A2: L is complete; :: thus M is complete LATTICE5
     M, L are_isomorphic by A1,WAYBEL_1:7;
   then consider f being map of M, L such that
A3: f is isomorphic by WAYBEL_1:def 8;
A4: f is one-to-one by A3,WAYBEL_0:66;
A5: rng f = the carrier of L by A3,WAYBEL_0:66;
A6: dom f = the carrier of M by FUNCT_2:def 1;
 let X be Subset of M;
  reconsider fX = f.:X as Subset of L;
  consider fa being Element of L such that
A7: fa is_<=_than fX and
A8: for fb being Element of L st fb is_<=_than fX holds fb <= fa
     by A2,LATTICE5:def 2;
   set a = (f qua Function)".fa;
     a in dom f by A4,A5,FUNCT_1:54;
   then reconsider a as Element of M;
A9: fa = f.a by A4,A5,FUNCT_1:57;
  take a;
  hereby let b be Element of M such that
 A10: b in X;
     reconsider fb = f.b as Element of L;
       fb in fX by A6,A10,FUNCT_1:def 12;
     then fa <= fb by A7,LATTICE3:def 8;
   hence a <= b by A3,A9,WAYBEL_0:66;
  end;
  let b be Element of M such that
A11: b is_<=_than X;
     reconsider fb = f.b as Element of L;
     fb is_<=_than fX proof let fc be Element of L; assume
     fc in fX;
      then consider c being set such that
  A12: c in dom f & c in X & fc = f.c by FUNCT_1:def 12;
      reconsider c as Element of M by A12;
        b <= c by A11,A12,LATTICE3:def 8;
    hence fb <= fc by A3,A12,WAYBEL_0:66;
   end;
   then fb <= fa by A8;
 hence b <= a by A3,A9,WAYBEL_0:66;
end;

theorem Th19:
 for L being non empty transitive RelStr, k being map of L, L
  st k is infs-preserving holds corestr k is infs-preserving
proof let L be non empty transitive RelStr,
          k be map of L, L such that
A1: k is infs-preserving;
 let X be Subset of L;
A2: k preserves_inf_of X by A1,WAYBEL_0:def 32;
    set f = corestr k;
A3: k = corestr k by WAYBEL_1:32;
 assume
A4: ex_inf_of X,L;
then A5: ex_inf_of k.:X, L by A2,WAYBEL_0:def 30;
A6: inf (k.:X) = k.inf X by A2,A4,WAYBEL_0:def 30;
A7: dom k = the carrier of L by FUNCT_2:def 1;
A8: rng k = the carrier of Image k by YELLOW_2:11; k.inf X in rng k by A7,
FUNCT_1:def 5;
then A9: k.inf X is Element of Image k by A8;
   reconsider fX = f.:X as Subset of Image k;
     "/\"(fX, L) is Element of Image k by A2,A3,A4,A9,WAYBEL_0:def 30;
 hence ex_inf_of f.:X, Image k by A3,A5,WAYBEL_8:20;
 thus inf (f.:X) = f.inf X by A3,A5,A6,WAYBEL_8:20;
end;

theorem
   for L being non empty transitive RelStr, k being map of L, L
  st k is filtered-infs-preserving
   holds corestr k is filtered-infs-preserving
proof let L be non empty transitive RelStr, k be map of L, L such that
A1: k is filtered-infs-preserving;
 let X be Subset of L; assume
   X is non empty filtered;
then A2: k preserves_inf_of X by A1,WAYBEL_0:def 36;
    set f = corestr k;
A3: k = corestr k by WAYBEL_1:32;
 assume
A4: ex_inf_of X,L;
then A5: ex_inf_of k.:X, L by A2,WAYBEL_0:def 30;
A6: inf (k.:X) = k.inf X by A2,A4,WAYBEL_0:def 30;
A7: dom k = the carrier of L by FUNCT_2:def 1;
A8: rng k = the carrier of Image k by YELLOW_2:11; k.inf X in rng k by A7,
FUNCT_1:def 5;
then A9: k.inf X is Element of Image k by A8;
   reconsider fX = f.:X as Subset of Image k;
     "/\"(fX, L) is Element of Image k by A2,A3,A4,A9,WAYBEL_0:def 30;
 hence ex_inf_of f.:X, Image k by A3,A5,WAYBEL_8:20;
 thus inf (f.:X) = f.inf X by A3,A5,A6,WAYBEL_8:20;
end;

theorem
   for L being non empty transitive RelStr, k being map of L, L
  st k is sups-preserving holds corestr k is sups-preserving
proof let L be non empty transitive RelStr, k be map of L, L such that
A1: k is sups-preserving;
 let X be Subset of L;
A2: k preserves_sup_of X by A1,WAYBEL_0:def 33;
    set f = corestr k;
A3: k = corestr k by WAYBEL_1:32;
 assume
A4: ex_sup_of X,L;
then A5: ex_sup_of k.:X, L by A2,WAYBEL_0:def 31;
A6: sup (k.:X) = k.sup X by A2,A4,WAYBEL_0:def 31;
A7: dom k = the carrier of L by FUNCT_2:def 1;
A8: rng k = the carrier of Image k by YELLOW_2:11; k.sup X in rng k by A7,
FUNCT_1:def 5;
then A9: k.sup X is Element of Image k by A8;
   reconsider fX = f.:X as Subset of Image k;
     "\/"(fX, L) is Element of Image k by A2,A3,A4,A9,WAYBEL_0:def 31;
 hence ex_sup_of f.:X, Image k by A3,A5,WAYBEL_8:19;
 thus sup (f.:X) = f.sup X by A3,A5,A6,WAYBEL_8:19;
end;

theorem Th22:
 for L being non empty transitive RelStr, k being map of L, L
  st k is directed-sups-preserving
   holds corestr k is directed-sups-preserving
proof let L be non empty transitive RelStr,
          k be map of L, L such that
A1: k is directed-sups-preserving;
 let X be Subset of L; assume
   X is non empty directed;
then A2: k preserves_sup_of X by A1,WAYBEL_0:def 37;
 set f = corestr k;
A3: k = corestr k by WAYBEL_1:32;
 assume
A4: ex_sup_of X,L;
then A5: ex_sup_of k.:X, L by A2,WAYBEL_0:def 31;
A6: sup (k.:X) = k.sup X by A2,A4,WAYBEL_0:def 31;
A7: dom k = the carrier of L by FUNCT_2:def 1;
A8: rng k = the carrier of Image k by YELLOW_2:11; k.sup X in rng k by A7,
FUNCT_1:def 5;
then A9: k.sup X is Element of Image k by A8;
   reconsider fX = f.:X as Subset of Image k;
     "\/"(fX, L) is Element of Image k by A2,A3,A4,A9,WAYBEL_0:def 31;
 hence ex_sup_of f.:X, Image k by A3,A5,WAYBEL_8:19;
 thus sup (f.:X) = f.sup X by A3,A5,A6,WAYBEL_8:19;
end;

canceled;

theorem Th24: :: Generalized YELLOW_2:19
for S, T being reflexive antisymmetric non empty RelStr,
    f being map of S, T
  st f is filtered-infs-preserving holds f is monotone
proof let S, T be reflexive antisymmetric non empty RelStr,
          f be map of S, T; assume
A1: f is filtered-infs-preserving;
  let x, y be Element of S such that
A2: x <= y;
A3:  x <= y & x <= x by A2;
then A4: {x, y} is_>=_than x by YELLOW_0:8;
    for b being Element of S st {x, y} is_>=_than b holds x >= b by YELLOW_0:8;
  then A5: x = inf {x, y} & ex_inf_of {x, y},S by A4,YELLOW_0:31;
    for a, b being Element of S st a in {x, y} & b in {x, y}
    ex z being Element of S st z in {x, y} & a >= z & b >= z
  proof
    let a, b be Element of S such that
  A6: a in {x, y} & b in {x, y};
    take x;
    thus x in {x, y} by TARSKI:def 2;
    thus a >= x & b >= x by A3,A6,TARSKI:def 2;
  end;
  then {x, y} is filtered non empty by WAYBEL_0:def 2;
then A7:  f preserves_inf_of {x, y} by A1,WAYBEL_0:def 36;
then A8: inf(f.:{x, y}) = f.x by A5,WAYBEL_0:def 30;
A9:  dom f = the carrier of S by FUNCT_2:def 1;
then A10: f.x = inf{f.x, f.y} by A8,FUNCT_1:118;
      f.:{x, y} = {f.x, f.y} by A9,FUNCT_1:118;
    then ex_inf_of {f.x, f.y}, T by A5,A7,WAYBEL_0:def 30;
    then {f.x, f.y} is_>=_than f.x by A10,YELLOW_0:def 10;
  hence f.x <= f.y by YELLOW_0:8;
end;

theorem Th25: ::  see YELLOW_2:17, for directed
 for S,T being non empty RelStr, f being map of S,T
  st f is monotone
   for X being Subset of S holds
    (X is filtered implies f.:X is filtered)
  proof let S,T be non empty RelStr, f be map of S,T;
  assume
A1: f is monotone;
   let X be Subset of S such that
A2: X is filtered;
   let x,y be Element of T; assume x in f.:X;
   then consider a being set such that
A3: a in the carrier of S & a in X & x = f.a by FUNCT_2:115;
   assume y in f.:X;
   then consider b being set such that
A4: b in the carrier of S & b in X & y = f.b by FUNCT_2:115;
   reconsider a,b as Element of S by A3,A4;
   consider c being Element of S such that
A5: c in X & c <= a & c <= b by A2,A3,A4,WAYBEL_0:def 2;
   take z = f.c;
   thus z in f.:X by A5,FUNCT_2:43;
   thus thesis by A1,A3,A4,A5,WAYBEL_1:def 2;
  end;

theorem Th26:
 for L1, L2, L3 being non empty RelStr, f be map of L1,L2, g be map of L2,L3
  st f is infs-preserving & g is infs-preserving
   holds g*f is infs-preserving
proof let L1, L2, L3 be non empty RelStr,
          f be map of L1,L2, g be map of L2,L3 such that
A1: f is infs-preserving and
A2: g is infs-preserving;
  set gf = g*f;
 let X be Subset of L1 such that
A3: ex_inf_of X, L1;
A4: dom f = the carrier of L1 by FUNCT_2:def 1;
  set gfX = gf.:X;
  set fX = f.:X;
A5: f preserves_inf_of X by A1,WAYBEL_0:def 32;
A6: g preserves_inf_of fX by A2,WAYBEL_0:def 32;
A7: gfX = g.:(f.:X) by RELAT_1:159;
A8: ex_inf_of fX, L2 by A3,A5,WAYBEL_0:def 30;
 hence ex_inf_of gfX, L3 by A6,A7,WAYBEL_0:def 30;
 thus inf gfX = g.inf fX by A6,A7,A8,WAYBEL_0:def 30
   .= g.(f.inf X) by A3,A5,WAYBEL_0:def 30
   .= gf.inf X by A4,FUNCT_1:23;
end;

theorem
   for L1, L2, L3 being non empty reflexive antisymmetric RelStr,
     f be map of L1,L2, g be map of L2,L3
  st f is filtered-infs-preserving & g is filtered-infs-preserving
   holds g*f is filtered-infs-preserving
proof let L1, L2, L3 be non empty reflexive antisymmetric RelStr,
          f be map of L1,L2, g be map of L2,L3 such that
A1: f is filtered-infs-preserving and
A2: g is filtered-infs-preserving;
  set gf = g*f;
 let X be Subset of L1 such that
A3: X is non empty filtered and
A4: ex_inf_of X, L1;
A5: dom f = the carrier of L1 by FUNCT_2:def 1;
  set gfX = gf.:X;
  set fX = f.:X;
A6: f preserves_inf_of X by A1,A3,WAYBEL_0:def 36;
    consider xx being Element of X;
      xx in X & X c= the carrier of L1 by A3;
then A7: f.xx in fX by FUNCT_2:43;
      f is monotone by A1,Th24;
    then fX is non empty filtered by A3,A7,Th25;
then A8: g preserves_inf_of fX by A2,WAYBEL_0:def 36;
A9: gfX = g.:(f.:X) by RELAT_1:159;
A10: ex_inf_of fX, L2 by A4,A6,WAYBEL_0:def 30;
 hence ex_inf_of gfX, L3 by A8,A9,WAYBEL_0:def 30;
 thus inf gfX = g.inf fX by A8,A9,A10,WAYBEL_0:def 30
   .= g.(f.inf X) by A4,A6,WAYBEL_0:def 30
   .= gf.inf X by A5,FUNCT_1:23;
end;

theorem
   for L1, L2, L3 being non empty RelStr, f be map of L1,L2, g be map of L2,L3
  st f is sups-preserving & g is sups-preserving
   holds g*f is sups-preserving
proof let L1, L2, L3 be non empty RelStr,
          f be map of L1,L2, g be map of L2,L3 such that
A1: f is sups-preserving and
A2: g is sups-preserving;
  set gf = g*f;
 let X be Subset of L1 such that
A3: ex_sup_of X, L1;
A4: dom f = the carrier of L1 by FUNCT_2:def 1;
  set gfX = gf.:X;
  set fX = f.:X;
A5: f preserves_sup_of X by A1,WAYBEL_0:def 33;
A6: g preserves_sup_of fX by A2,WAYBEL_0:def 33;
A7: gfX = g.:(f.:X) by RELAT_1:159;
A8: ex_sup_of fX, L2 by A3,A5,WAYBEL_0:def 31;
 hence ex_sup_of gfX, L3 by A6,A7,WAYBEL_0:def 31;
 thus sup gfX = g.sup fX by A6,A7,A8,WAYBEL_0:def 31
   .= g.(f.sup X) by A3,A5,WAYBEL_0:def 31
   .= gf.sup X by A4,FUNCT_1:23;
end;

theorem   :: see also WAYBEL15:13
   for L1, L2, L3 being non empty reflexive antisymmetric RelStr,
     f be map of L1,L2, g be map of L2,L3
  st f is directed-sups-preserving & g is directed-sups-preserving
   holds g*f is directed-sups-preserving
proof let L1, L2, L3 be non empty reflexive antisymmetric RelStr,
          f be map of L1,L2, g be map of L2,L3 such that
A1: f is directed-sups-preserving and
A2: g is directed-sups-preserving;
  set gf = g*f;
 let X be Subset of L1 such that
A3: X is non empty directed and
A4: ex_sup_of X, L1;
A5: dom f = the carrier of L1 by FUNCT_2:def 1;
  set gfX = gf.:X;
  set fX = f.:X;
A6: f preserves_sup_of X by A1,A3,WAYBEL_0:def 37;
    consider xx being Element of X;
      xx in X & X c= the carrier of L1 by A3;
then A7: f.xx in fX by FUNCT_2:43;
      f is monotone by A1,WAYBEL17:3;
    then fX is non empty directed by A3,A7,YELLOW_2:17;
then A8: g preserves_sup_of fX by A2,WAYBEL_0:def 37;
A9: gfX = g.:(f.:X) by RELAT_1:159;
A10: ex_sup_of fX, L2 by A4,A6,WAYBEL_0:def 31;
 hence ex_sup_of gfX, L3 by A8,A9,WAYBEL_0:def 31;
 thus sup gfX = g.sup fX by A8,A9,A10,WAYBEL_0:def 31
   .= g.(f.sup X) by A4,A6,WAYBEL_0:def 31
   .= gf.sup X by A5,FUNCT_1:23;
end;

begin :: Some remarks on lattice product

theorem
   for I being non empty set
 for J being RelStr-yielding non-Empty ManySortedSet of I
  st for i being Element of I holds J.i is lower-bounded antisymmetric RelStr
   holds product J is lower-bounded
proof let I be non empty set,
          J be RelStr-yielding non-Empty ManySortedSet of I such that
A1: for i being Element of I holds J.i is lower-bounded antisymmetric RelStr;
   deffunc F(Element of I) = Bottom (J.$1);
   consider f being ManySortedSet of I such that
A2: for i being Element of I holds f.i = F(i) from LambdaDMS;
A3: dom f = I by PBOOLE:def 3;
      now let i be Element of I; f.i = Bottom (J.i) by A2;
     hence f.i is Element of J.i;
    end;
   then reconsider f as Element of product J by A3,WAYBEL_3:27;
  take f;
  let b be Element of product J such that b in the carrier of product J;
     now let i be Element of I;
   A4:  f.i = Bottom (J.i) by A2;
          J.i is lower-bounded antisymmetric non empty RelStr by A1;
    hence f.i <= b.i by A4,YELLOW_0:44;
   end;
  hence f <= b by WAYBEL_3:28;
end;

theorem
   for I being non empty set
 for J being RelStr-yielding non-Empty ManySortedSet of I
  st for i being Element of I holds J.i is upper-bounded antisymmetric RelStr
   holds product J is upper-bounded
proof let I be non empty set,
          J be RelStr-yielding non-Empty ManySortedSet of I such that
A1: for i being Element of I holds J.i is upper-bounded antisymmetric RelStr;
   deffunc F(Element of I) = Top (J.$1);
   consider f being ManySortedSet of I such that
A2: for i being Element of I holds f.i = F(i) from LambdaDMS;
A3: dom f = I by PBOOLE:def 3;
      now let i be Element of I; f.i = Top (J.i) by A2;
     hence f.i is Element of J.i;
    end;
   then reconsider f as Element of product J by A3,WAYBEL_3:27;
  take f;
  let b be Element of product J such that b in the carrier of product J;
     now let i be Element of I;
   A4:  f.i = Top (J.i) by A2;
          J.i is upper-bounded antisymmetric non empty RelStr by A1;
    hence f.i >= b.i by A4,YELLOW_0:45;
   end;
  hence f >= b by WAYBEL_3:28;
end;

theorem
   for I being non empty set
 for J being RelStr-yielding non-Empty ManySortedSet of I
  st for i being Element of I holds J.i is lower-bounded antisymmetric RelStr
   holds for i being Element of I holds Bottom (product J).i = Bottom (J.i)
proof let I be non empty set,
          J be RelStr-yielding non-Empty ManySortedSet of I such that
A1: for i being Element of I holds J.i is lower-bounded antisymmetric RelStr;
   deffunc F(Element of I) = Bottom (J.$1);
   consider f being ManySortedSet of I such that
A2: for i being Element of I holds f.i = F(i) from LambdaDMS;
A3: dom f = I by PBOOLE:def 3;
      now let i be Element of I; f.i = Bottom (J.i) by A2;
     hence f.i is Element of J.i;
    end;
   then reconsider f as Element of product J by A3,WAYBEL_3:27;
A4: {} is_<=_than f by YELLOW_0:6;
A5: now let b be Element of product J such that {} is_<=_than b;
         now let i be Element of I;
     A6:  f.i = Bottom (J.i) by A2;
            J.i is lower-bounded antisymmetric non empty RelStr by A1;
      hence f.i <= b.i by A6,YELLOW_0:44;
     end;
     hence f <= b by WAYBEL_3:28;
    end;
      now let c be Element of product J such that {} is_<=_than c and
  A7: for b being Element of product J st {} is_<=_than b holds b >= c;
  A8: c <= f by A4,A7;
        for i being Element of I holds J.i is antisymmetric by A1;
  then A9: product J is antisymmetric by WAYBEL_3:30;
         now let i be Element of I;
     A10:  f.i = Bottom (J.i) by A2;
            J.i is lower-bounded antisymmetric non empty RelStr by A1;
      hence f.i <= c.i by A10,YELLOW_0:44;
     end;
     then f <= c by WAYBEL_3:28;
     hence c = f by A8,A9,YELLOW_0:def 3;
    end;
then A11: ex_sup_of {}, product J by A4,A5,YELLOW_0:def 7;
     now let a be Element of product J such that {} is_<=_than a;
       now let i be Element of I;
   A12:  f.i = Bottom (J.i) by A2;
          J.i is lower-bounded antisymmetric non empty RelStr by A1;
      hence f.i <= a.i by A12,YELLOW_0:44;
     end;
    hence f <= a by WAYBEL_3:28;
   end;
   then f = "\/"({}, product J) by A4,A11,YELLOW_0:def 9;
then A13: Bottom (product J) = f by YELLOW_0:def 11;
 let i be Element of I;
 thus Bottom (product J).i = Bottom (J.i) by A2,A13;
end;

theorem
   for I being non empty set
 for J being RelStr-yielding non-Empty ManySortedSet of I
  st for i being Element of I holds J.i is upper-bounded antisymmetric RelStr
   holds for i being Element of I holds Top (product J).i = Top (J.i)
proof let I be non empty set,
          J be RelStr-yielding non-Empty ManySortedSet of I such that
A1: for i being Element of I holds J.i is upper-bounded antisymmetric RelStr;
   deffunc F(Element of I) = Top (J.$1);
   consider f being ManySortedSet of I such that
A2: for i being Element of I holds f.i = F(i) from LambdaDMS;
A3: dom f = I by PBOOLE:def 3;
      now let i be Element of I; f.i = Top (J.i) by A2;
     hence f.i is Element of J.i;
    end;
   then reconsider f as Element of product J by A3,WAYBEL_3:27;
A4: {} is_>=_than f by YELLOW_0:6;
A5: now let b be Element of product J such that {} is_>=_than b;
         now let i be Element of I;
     A6:  f.i = Top (J.i) by A2;
            J.i is upper-bounded antisymmetric non empty RelStr by A1;
      hence f.i >= b.i by A6,YELLOW_0:45;
     end;
     hence f >= b by WAYBEL_3:28;
    end;
      now let c be Element of product J such that {} is_>=_than c and
  A7: for b being Element of product J st {} is_>=_than b holds b <= c;
  A8: c >= f by A4,A7;
        for i being Element of I holds J.i is antisymmetric by A1;
  then A9: product J is antisymmetric by WAYBEL_3:30;
         now let i be Element of I;
     A10:  f.i = Top (J.i) by A2;
            J.i is upper-bounded antisymmetric non empty RelStr by A1;
      hence f.i >= c.i by A10,YELLOW_0:45;
     end;
     then f >= c by WAYBEL_3:28;
     hence c = f by A8,A9,YELLOW_0:def 3;
    end;
then A11: ex_inf_of {}, product J by A4,A5,YELLOW_0:def 8;
     now let a be Element of product J such that {} is_>=_than a;
       now let i be Element of I;
   A12:  f.i = Top (J.i) by A2;
          J.i is upper-bounded antisymmetric non empty RelStr by A1;
      hence f.i >= a.i by A12,YELLOW_0:45;
     end;
    hence f >= a by WAYBEL_3:28;
   end;
   then f = "/\"({}, product J) by A4,A11,YELLOW_0:def 10;
then A13: Top (product J) = f by YELLOW_0:def 12;
 let i be Element of I;
 thus Top (product J).i = Top (J.i) by A2,A13;
end;

theorem :: Theorem 2.7, p. 60, (i)
   :: The hint in CCL suggest employing the distributivity equations.
   :: However, we prove it directly from the definition of continuity;
   :: it seems easier to do so.

  for I being non empty set,
    J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I
 st for i being Element of I holds J.i is continuous complete LATTICE
  holds product J is continuous
proof let I be non empty set,
      J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I
  such that
A1: for i being Element of I holds J.i is continuous complete LATTICE;
  set pJ = product J;

A2: for i being Element of I holds J.i is complete LATTICE by A1;
  then reconsider pJ' = pJ as complete LATTICE by WAYBEL_3:31;

  hereby let x be Element of pJ;
     reconsider x' = x as Element of pJ';
       waybelow x' is non empty;
   hence waybelow x is non empty;
       waybelow x' is directed;
   hence waybelow x is directed;
  end;
     pJ' is up-complete;
  hence pJ is up-complete;
  let x be Element of pJ;
 set swx = sup waybelow x;
     now
    thus dom x = I by WAYBEL_3:27;
    thus dom swx = I by WAYBEL_3:27;
    let i be set; assume
     i in I;
      then reconsider i' = i as Element of I;
  A3: swx.i' = sup pi(waybelow x, i') by A2,WAYBEL_3:32;
        now let a be set;
       hereby assume a in pi(waybelow x, i');
         then consider f being Function such that
     A4: f in waybelow x and
     A5: a = f.i by CARD_3:def 6;
         reconsider f as Element of pJ by A4;
           f << x by A4,WAYBEL_3:7;
         then f.i' << x.i' by A2,WAYBEL_3:33;
        hence a in waybelow x.i' by A5,WAYBEL_3:7;
       end;
       assume
     A6: a in waybelow x.i';
       deffunc F(Element of I) = Bottom (J.$1);
       consider g being ManySortedSet of I such that
     A7: for i being Element of I holds g.i = F(i) from LambdaDMS;
     A8: dom g = I by PBOOLE:def 3;
       set f = g+*(i, a);
     A9: dom f = I by A8,FUNCT_7:32;
       now let j be Element of I;
          per cases;
          suppose A10: i' = j;
              f.i' = a by A8,FUNCT_7:33;
           hence f.j is Element of J.j by A6,A10;
          suppose i' <> j; then f.j = g.j by FUNCT_7:34 .= Bottom (J.j) by A7
;
           hence f.j is Element of J.j;
         end;
       then reconsider f as Element of pJ by A9,WAYBEL_3:27;
     A11: now let j be Element of I;
          per cases;
          suppose A12: i' = j;
        f.i' = a by A8,FUNCT_7:33;
           hence f.j << x.j by A6,A12,WAYBEL_3:7;
          suppose A13: i' <> j;
      A14: J.j is complete LATTICE by A1;
              f.j = g.j by A13,FUNCT_7:34 .= Bottom (J.j) by A7;
           hence f.j << x.j by A14,WAYBEL_3:4;
         end;
         reconsider K = {i'} as finite Subset of I;
       now let j be Element of I; assume not j in K;
           then j <> i' by TARSKI:def 1;
          hence f.j = g.j by FUNCT_7:34 .= Bottom (J.j) by A7;
         end;
         then f << x by A2,A11,WAYBEL_3:33;
     then A15: f in waybelow x by WAYBEL_3:7;
        a = f.i' by A8,FUNCT_7:33;
       hence a in pi(waybelow x, i') by A15,CARD_3:def 6;
      end;
  then A16: pi(waybelow x, i') = waybelow (x.i') by TARSKI:2;
        J.i' is satisfying_axiom_of_approximation by A1;
    hence x.i = swx.i by A3,A16,WAYBEL_3:def 5;
   end;
  hence x = sup waybelow x by FUNCT_1:9;
end;

begin :: Kernel projections and quotient lattices

theorem Th35: :: Proposition 2.8 p. 61
for L, T being continuous complete LATTICE, g being CLHomomorphism of L, T,
    S being Subset of [:L, L:]
 st S = [:g, g:]"(id the carrier of T)
  holds subrelstr S is CLSubFrame of [:L, L:]
proof let L, T be continuous complete LATTICE,
          g be CLHomomorphism of L, T,
          SL be Subset of [:L, L:] such that
A1: SL = [:g, g:]"(id the carrier of T);
A2: g is infs-preserving directed-sups-preserving by WAYBEL16:def 1;
   set pL = [:L, L:], pg = [:g, g:], pT = [:T, T:];
   consider x being Element of L;
A3: dom g = the carrier of L by FUNCT_2:def 1;
 then A4: [x, x] in [:dom g, dom g:] by ZFMISC_1:106;
 A5: dom [:g, g:] = [: dom g, dom g :] by FUNCT_3:def 9;
       [g.x, g.x] in id the carrier of T by RELAT_1:def 10;
     then [:g, g:].[x, x] in id the carrier of T by A3,FUNCT_3:def 9;
   then reconsider nSL = SL as non empty Subset of [:L, L:] by
A1,A4,A5,FUNCT_1:def 13;
A6: subrelstr nSL is non empty;

A7: the carrier of pL=[:the carrier of L,the carrier of L:] by YELLOW_3:def 2;

A8: subrelstr SL is infs-inheriting proof
    let X be Subset of subrelstr SL such that
 A9: ex_inf_of X, pL;
       X c= the carrier of subrelstr SL;
 then A10: X c= SL by YELLOW_0:def 15;
      then X c= the carrier of pL by XBOOLE_1:1;
    then reconsider X' = X as Subset of pL;
    consider x, y being set such that
 A11: x in the carrier of L & y in the carrier of L and
 A12: inf X' = [x, y] by A7,ZFMISC_1:def 2;
       pg is infs-preserving by A2,Th9;
     then pg preserves_inf_of X' by WAYBEL_0:def 32;
 then A13: ex_inf_of pg.:X', pT & inf (pg.:X')=pg.inf X' by A9,WAYBEL_0:def 30;
 A14: pg.:X c= pg.:SL by A10,RELAT_1:156;
        pg.:SL c= id the carrier of T by A1,FUNCT_1:145;
 then A15: pg.:X' c= id the carrier of T by A14,XBOOLE_1:1;
       ex_inf_of pg.:X', [:T, T:] by YELLOW_0:17;
 then A16: inf (pg.:X') in id the carrier of T by A15,Th13;
       [x, y] in [:dom g, dom g:] by A3,A11,ZFMISC_1:106;
 then [x, y] in dom [:g, g:] by FUNCT_3:def 9;
     then [x, y] in [:g, g:]"(id the carrier of T) by A12,A13,A16,FUNCT_1:def
13;
    hence "/\"
(X, pL) in the carrier of subrelstr SL by A1,A12,YELLOW_0:def 15;
   end;

  subrelstr SL is directed-sups-inheriting proof
    let X be directed Subset of subrelstr SL such that
 A17: X <> {} and
 A18: ex_sup_of X, pL;
       X c= the carrier of subrelstr SL;
 then A19: X c= SL by YELLOW_0:def 15;
   reconsider X' = X as directed non empty Subset of pL by A6,A17,YELLOW_2:7;
   consider x, y being set such that
 A20: x in the carrier of L & y in the carrier of L and
 A21: sup X' = [x, y] by A7,ZFMISC_1:def 2;
       pg is directed-sups-preserving by A2,Th12;
     then pg preserves_sup_of X' by WAYBEL_0:def 37;
 then A22: ex_sup_of pg.:X', pT & sup (pg.:X')=pg.sup X' by A18,WAYBEL_0:def 31
;
 A23: pg.:X c= pg.:SL by A19,RELAT_1:156;
        pg.:SL c= id the carrier of T by A1,FUNCT_1:145;
 then A24: pg.:X' c= id the carrier of T by A23,XBOOLE_1:1;
       ex_sup_of pg.:X', [:T, T:] by YELLOW_0:17;
 then A25: sup (pg.:X') in id the carrier of T by A24,Th14;
       [x, y] in [:dom g, dom g:] by A3,A20,ZFMISC_1:106;
 then [x, y] in dom [:g, g:] by FUNCT_3:def 9;
     then [x, y] in [:g, g:]"(id the carrier of T) by A21,A22,A25,FUNCT_1:def
13;
    hence "\/"
(X, pL) in the carrier of subrelstr SL by A1,A21,YELLOW_0:def 15;
   end;
 hence subrelstr SL is CLSubFrame of [:L, L:] by A6,A8;
end;

:: Proposition 2.9, p. 61, see WAYBEL10

:: Lemma 2.10, p. 61, see WAYBEL15:16

definition
 let L be RelStr, R be Subset of [:L, L:] such that
A1: R is Equivalence_Relation of the carrier of L;
 func EqRel R -> Equivalence_Relation of the carrier of L equals
:Def1:   R;
 correctness by A1;
end;

definition :: Definition 2.12, p. 62, part I (congruence)
 let L be non empty RelStr, R be Subset of [:L, L:];
 attr R is CLCongruence means :Def2:
  R is Equivalence_Relation of the carrier of L &
  subrelstr R is CLSubFrame of [:L, L:];
end;

theorem Th36:
 for L being complete LATTICE, R being non empty Subset of [:L, L:]
  st R is CLCongruence
   for x be Element of L holds [inf Class(EqRel R, x), x] in R
proof let L be complete LATTICE,
     R be non empty Subset of [:L, L:]; assume
A1: R is CLCongruence;
then A2: R is Equivalence_Relation of the carrier of L by Def2;
 A3: subrelstr R is CLSubFrame of [:L, L:] by A1,Def2;
A4: R = EqRel R by A2,Def1;

   let x be Element of L;
       set CRx = Class(EqRel R, x);
       reconsider SR = [:CRx, {x}:] as Subset of [:L, L:];
         SR c= the carrier of subrelstr R proof let a be set; assume
            a in SR; then consider a1, a2 being set such that
       A5: a1 in CRx & a2 in {x} & a = [a1, a2] by ZFMISC_1:def 2;
             a2 = x by A5,TARSKI:def 1;
          then a in R by A4,A5,EQREL_1:27;
        hence a in the carrier of subrelstr R by YELLOW_0:def 15;
       end;
       then reconsider SR' = SR as Subset of subrelstr R;
   A6: x in CRx by EQREL_1:28;
   A7:  ex_inf_of SR, [:L, L:] by YELLOW_0:17;
   then A8:  inf SR = [inf proj1 SR, inf proj2 SR] by Th7
       .= [inf CRx, inf proj2 SR] by FUNCT_5:11
       .= [inf CRx, inf {x}] by A6,FUNCT_5:11
       .= [inf CRx, x] by YELLOW_0:39;
         "/\"(SR', [:L, L:]) in the carrier of subrelstr R
              by A3,A7,YELLOW_0:def 18;
     hence [inf CRx, x] in R by A8,YELLOW_0:def 15;
   end;

definition :: Theorem 2.11, p. 61-62, (1) implies (3) (part a)
 let L be complete LATTICE, R be non empty Subset of [:L, L:] such that
A1: R is CLCongruence;
 func kernel_op R -> kernel map of L, L means
:Def3: for x being Element of L holds it.x = inf Class(EqRel R, x);
 existence proof
A2: R is Equivalence_Relation of the carrier of L by A1,Def2;
 A3: subrelstr R is CLSubFrame of [:L, L:] by A1,Def2;
  deffunc F(Element of L) = inf Class(EqRel R, $1);
  consider k being Function of the carrier of L, the carrier of L such that
A4: for x being Element of L holds k.x = F(x)
      from LambdaD;
A5: R = EqRel R by A2,Def1;
  reconsider k as map of L, L;
A6: k is projection proof
       now let x be Element of L;
       set CRx = Class(EqRel R, x);
   A7: k.x = inf CRx by A4;
   then A8: k.(k.x) = inf Class(EqRel R, inf CRx) by A4;
         [inf CRx, x] in R by A1,Th36;
       then inf CRx in CRx by A5,EQREL_1:27;
   then Class(EqRel R, inf CRx) = CRx by EQREL_1:31;
      hence (k*k).x
          = k.x by A7,A8,FUNCT_2:21;
     end;
     then k*k = k by FUNCT_2:113;
    hence k is idempotent by QUANTAL1:def 9;
    thus k is monotone proof :: WAYBEL_1:def 2
     let x, y be Element of L such that
   A9: x <= y;
   A10: inf {x, y} = x"/\"y by YELLOW_0:40 .= x by A9,YELLOW_0:25;
       set CRx = Class(EqRel R, x);
       set CRy = Class(EqRel R, y);
       reconsider SR = {[inf CRx, x], [inf CRy, y]} as Subset of [:L, L:];
         [inf CRx, x] in R & [inf CRy, y] in R by A1,Th36;
       then SR c= R by ZFMISC_1:38;
       then SR c= the carrier of subrelstr R by YELLOW_0:def 15;
       then reconsider SR' = SR as Subset of subrelstr R;
   A11: ex_inf_of SR, [:L, L:] by YELLOW_0:17;
   then A12: inf SR = [inf proj1 SR, inf proj2 SR] by Th7
        .= [inf {inf CRx, inf CRy}, inf proj2 SR] by FUNCT_5:16
        .= [inf {inf CRx, inf CRy}, inf {x, y}] by FUNCT_5:16;
         "/\"(SR', [:L, L:]) in the carrier of subrelstr R
            by A3,A11,YELLOW_0:def 18;
       then [inf {inf CRx, inf CRy}, x] in R by A10,A12,YELLOW_0:def 15;
       then inf {inf CRx, inf CRy} in CRx by A5,EQREL_1:27;
   then A13: inf CRx <= inf {inf CRx, inf CRy} by YELLOW_2:24;
         inf CRy in {inf CRx, inf CRy} by TARSKI:def 2;
   then A14: inf {inf CRx, inf CRy} <= inf CRy by YELLOW_2:24;
      k.x = inf CRx & k.y = inf CRy by A4;
      hence k.x <= k.y by A13,A14,YELLOW_0:def 2;
    end;
   end;
     now let x be Element of L;
   A15: k.x = inf Class(EqRel R, x) by A4;
       set CRx = Class(EqRel R, x);
   A16: x in CRx by EQREL_1:28;
        inf CRx is_<=_than CRx by YELLOW_0:33;
      then inf CRx <= x by A16,LATTICE3:def 8;
    hence k.x <= id(L).x by A15,GRCAT_1:11;
   end;
   then k <= id (L) by YELLOW_2:10;
  then reconsider k as kernel map of L, L by A6,WAYBEL_1:def 15;
  take k;
  thus thesis by A4;
end;
 uniqueness proof let it1, it2 be kernel map of L, L such that
A17: for x being Element of L holds it1.x = inf Class(EqRel R, x) and
A18: for x being Element of L holds it2.x = inf Class(EqRel R, x);
     now let x be set; assume x in the carrier of L;
     then reconsider x' = x as Element of L;
    thus it1.x = inf Class(EqRel R, x') by A17 .= it2.x by A18;
   end;
  hence it1 = it2 by FUNCT_2:18;
 end;
end;

theorem Th37: :: Theorem 2.11, p. 61-62, (1) implies (3) (part b)
 for L being complete LATTICE, R be non empty Subset of [:L, L:]
  st R is CLCongruence
   holds kernel_op R is directed-sups-preserving &
         R = [:kernel_op R, kernel_op R:]"(id the carrier of L)
proof let L be complete LATTICE,
          R be non empty Subset of [:L, L:]; assume
A1: R is CLCongruence;
then A2: R is Equivalence_Relation of the carrier of L by Def2;
then A3: EqRel R = R by Def1;
A4: subrelstr R is CLSubFrame of [:L, L:] by A1,Def2;
   set k = kernel_op R; set cL = the carrier of L;
A5: dom k = cL by FUNCT_2:def 1;
 thus k is directed-sups-preserving proof
  let D be Subset of L such that
 A6: D is non empty directed and ex_sup_of D, L;
  thus ex_sup_of k.:D, L by YELLOW_0:17;
   set d = sup D; set ds = sup (k.:D);
     k.:D is_<=_than k.d proof let b be Element of L; assume
     b in k.:D;
      then consider a being set such that
  A7: a in dom k & a in D & b = k.a by FUNCT_1:def 12;
      reconsider a as Element of L by A7;
        D is_<=_than d by YELLOW_0:32;
      then a <= d by A7,LATTICE3:def 9;
    hence b <= k.d by A7,WAYBEL_1:def 2;
   end;
 then A8: ds <= k.d by YELLOW_0:32;
   set S = {[k.x, x] where x is Element of L : x in D};
 A9: the carrier of subrelstr R = R by YELLOW_0:def 15;
 A10: S c= R proof let x be set; assume x in S;
        then consider a being Element of L such that
    A11: x = [k.a, a] & a in D;
          k.a = inf Class(EqRel R, a) by A1,Def3;
       hence x in R by A1,A11,Th36;
      end;
   then reconsider S' = S as Subset of subrelstr R by A9;
        S c= the carrier of [:L, L:] by A10,XBOOLE_1:1;
   then reconsider S as Subset of [:L, L:];
 A12: ex_sup_of S, [:L, L:] by YELLOW_0:17;
     consider e being set such that
 A13: e in D by A6,XBOOLE_0:def 1;
     reconsider e as Element of L by A13;
  A14: [k.e, e] in S by A13;
 A15: S' is directed proof let x, y be Element of subrelstr R; assume
    A16: x in S' & y in S';
        then consider a being Element of L such that
    A17: x = [k.a, a] & a in D;
        consider b being Element of L such that
    A18: y = [k.b, b] & b in D by A16;
        consider c being Element of L such that
    A19: c in D & a <= c & b <= c by A6,A17,A18,WAYBEL_0:def 1;
        set z = [k.c, c];
          z in S' by A19;
        then reconsider z as Element of subrelstr R;
       take z;
       thus z in S' by A19;
          k.a <= k.c by A19,WAYBEL_1:def 2;
        then [k.a, a] <= [k.c, c] by A19,YELLOW_3:11;
       hence x <= z by A17,YELLOW_0:61;
          k.b <= k.c by A19,WAYBEL_1:def 2;
        then [k.b, b] <= [k.c, c] by A19,YELLOW_3:11;
       hence y <= z by A18,YELLOW_0:61;
      end;
        now let x be set;
       hereby assume x in proj1 S; then consider y being set such that
      A20: [x, y] in S by FUNCT_5:def 1;
          consider a being Element of L such that
      A21: [x, y] = [k.a, a] & a in D by A20;
            x = k.a by A21,ZFMISC_1:33;
        hence x in k.:D by A5,A21,FUNCT_1:def 12;
       end;
       assume x in k.:D; then consider y being set such that
      A22: y in dom k & y in D & x = k.y by FUNCT_1:def 12;
          reconsider y as Element of L by A22;
            [k.y, y] in S by A22;
       hence x in proj1 S by A22,FUNCT_5:def 1;
      end;
 then A23: proj1 S = k.:D by TARSKI:2;
        now let x be set;
       hereby assume x in proj2 S; then consider y being set such that
      A24: [y, x] in S by FUNCT_5:def 2;
          consider a being Element of L such that
      A25: [y, x] = [k.a, a] & a in D by A24;
        thus x in D by A25,ZFMISC_1:33;
       end;
       assume
      A26: x in D;
        then reconsider x' = x as Element of L;
          [k.x', x'] in S by A26;
       hence x in proj2 S by FUNCT_5:def 2;
      end;
 then proj2 S = D by TARSKI:2;
  then sup S = [ds, d] by A12,A23,Th8;
   then [ds, d] in R by A4,A9,A12,A14,A15,WAYBEL_0:def 4;
 then A27: ds in Class(EqRel R, d) by A3,EQREL_1:27;
      k.d = inf Class(EqRel R, d) by A1,Def3;
    then k.d <= ds by A27,YELLOW_2:24;
  hence sup (k.:D) = k.sup D by A8,YELLOW_0:def 3;
 end;
    now let x be set;
   hereby assume
  A28: x in R; then x in the carrier of [:L, L:];
     then x in [:cL, cL:] by YELLOW_3:def 2;
     then consider x1, x2 being set such that
  A29: x1 in cL & x2 in cL & x = [x1, x2] by ZFMISC_1:def 2;
    reconsider x1, x2 as Element of L by A29;
  A30: k.x1=inf Class(EqRel R, x1) & k.x2 = inf Class(EqRel R, x2) by A1,Def3;
        x1 in Class(EqRel R, x2) by A3,A28,A29,EQREL_1:27;
      then k.x1 = k.x2 by A30,EQREL_1:31;
  then A31: [k.x1, k.x2] in id cL by RELAT_1:def 10;
  A32: [:k, k:].[x1, x2] = [k.x1, k.x2] by A5,FUNCT_3:def 9;
        dom [:k, k:] = [:dom k, dom k:] by FUNCT_3:def 9;
      then [x1, x2] in dom [:k, k:] by A5,ZFMISC_1:106;
    hence x in [:k, k:]"(id cL) by A29,A31,A32,FUNCT_1:def 13;
   end;
   assume x in [:k, k:]"(id cL);
  then A33: x in dom [:k, k:] & [:k, k:].x in id cL by FUNCT_1:def 13;
      then x in [:dom k, dom k:] by FUNCT_3:def 9;
      then consider x1, x2 being set such that
  A34: x1 in dom k & x2 in dom k & x = [x1, x2] by ZFMISC_1:def 2;
      reconsider x1, x2 as Element of L by A34;
        [:k, k:].[x1, x2] = [k.x1, k.x2] by A34,FUNCT_3:def 9;
  then A35: k.x1 = k.x2 by A33,A34,RELAT_1:def 10;
     k.x1=inf Class(EqRel R, x1) & k.x2 = inf Class(EqRel R, x2) by A1,Def3;
  then A36: [k.x1, x1] in R & [k.x2, x2] in R by A1,Th36;
      then [x1, k.x1] in R by A2,EQREL_1:12;
   hence x in R by A2,A34,A35,A36,EQREL_1:13;
  end;
 hence R = [:k, k:]"(id cL) by TARSKI:2;
end;

theorem Th38: :: Theorem 2.11, p. 61-62, (3) implies (2)
 for L being continuous complete LATTICE, R be Subset of [:L, L:],
     k being kernel map of L, L
  st k is directed-sups-preserving & R = [:k, k:]"(id the carrier of L)
   ex LR being continuous complete strict LATTICE st
     the carrier of LR = Class EqRel R &
     the InternalRel of LR = {[Class(EqRel R, x), Class(EqRel R, y)]
                                where x, y is Element of L : k.x <= k.y } &
     for g being map of L, LR
      st for x being Element of L holds g.x = Class(EqRel R, x)
       holds g is CLHomomorphism of L, LR
proof let L be continuous complete LATTICE,
          R be Subset of [:L, L:], k be kernel map of L, L such that
A1: k is directed-sups-preserving and
A2: R = [:k, k:]"(id the carrier of L);
A3: R is Equivalence_Relation of the carrier of L by A2,Th2;
   set ER = EqRel R;
A4: ER = R by A3,Def1;
   set cL = the carrier of L;
A5: dom k = cL by FUNCT_2:def 1;
then A6: dom [:k, k:] = [:cL, cL:] by FUNCT_3:def 9;
   consider xx being Element of L;
     Class(ER, xx) in Class ER by EQREL_1:def 5;
   then reconsider CER = Class ER as non empty Subset-Family of cL;

   defpred P[set,set] means
     ex x, y being Element of L st
      $1 = Class(ER, x) & $2 = Class(ER, y) & k.x <= k.y;
   consider LR being non empty strict RelStr such that
A7: the carrier of LR = CER and
A8: for a, b being Element of LR holds a <= b iff P[a,b] from RelStrEx;
A9: for a, b being Element of cL holds
       Class(ER, a) = Class(ER, b) iff k.a = k.b proof
      let a, b be Element of cL;
      hereby assume
        Class(ER, a) = Class(ER, b);
         then a in Class(ER, b) by EQREL_1:31;
         then [a, b] in R by A4,EQREL_1:27;
         then [:k, k:].[a, b] in id cL by A2,FUNCT_1:def 13;
         then [k.a, k.b] in id cL by A5,FUNCT_3:def 9;
       hence k.a = k.b by RELAT_1:def 10;
      end;
     A10: [a, b] in [:cL, cL:] by ZFMISC_1:def 2;
      assume k.a = k.b;
         then [k.a, k.b] in id cL by RELAT_1:def 10;
         then [:k, k:].[a, b] in id cL by A5,FUNCT_3:def 9;
         then [a, b] in ER by A2,A4,A6,A10,FUNCT_1:def 13;
         then a in Class(ER, b) by EQREL_1:27;
      hence Class(ER, a) = Class(ER, b) by EQREL_1:31;
     end;
    reconsider rngk = rng k as non empty set;
    defpred P[set, set] means
     ex a being Element of cL st $1 = Class(ER, a) & $2 = k.a;
A11: for x being Element of CER ex y being Element of rngk st P[x, y] proof
      let x be Element of CER;
       consider y being set such that
    A12: y in cL & x = Class(ER, y) by EQREL_1:def 5;
       reconsider y as Element of L by A12;
       reconsider ky = k.y as Element of rngk by A5,FUNCT_1:def 5;
       take ky;
       thus P[x, ky] by A12;
    end;
    consider f being Function of CER, rngk such that
A13: for x being Element of CER holds P[x, f.x] from FuncExD(A11);
A14: dom f = CER by FUNCT_2:def 1;

A15: for x being Element of L holds f.Class(ER, x) = k.x proof
      let x be Element of L;
      reconsider CERx = Class(ER, x) as Element of CER by EQREL_1:def 5;
      consider a being Element of cL such that
     A16: CERx = Class(ER, a) & f.CERx = k.a by A13;
      thus f.Class(ER, x) = k.x by A9,A16;
     end;

    set tIR = the InternalRel of LR;
    set IR = {[Class(ER, x), Class(ER, y)]
                  where x, y is Element of L : k.x <= k.y };

A17: for x being Element of LR ex a being Element of L st x = Class(ER, a)
     proof let x be Element of LR;
           x in CER by A7; then consider a being set such that
     A18: a in cL & x = Class(ER, a) by EQREL_1:def 5;
       reconsider a as Element of L by A18;
      take a;
      thus x = Class(ER, a) by A18;
     end;

       now let x1, x2 be set; assume
   A19: x1 in CER & x2 in CER & f.x1 = f.x2;
       then reconsider x1' = x1 as Element of LR by A7;
       reconsider x2' = x2 as Element of LR by A7,A19;
       consider a being Element of L such that
   A20: x1' = Class(ER, a) by A17;
       consider b being Element of L such that
   A21: x2' = Class(ER, b) by A17;
         f.x1' = k.a & f.x2' = k.b by A15,A20,A21;
      hence x1 = x2 by A9,A19,A20,A21;
     end;
then A22:  f is one-to-one by FUNCT_2:25;

A23:  the carrier of Image k = rngk by YELLOW_2:11;
     then reconsider f as map of LR, Image k by A7;

       now let y be set;
      hereby assume y in rng f; then consider x being set such that
     A24: x in dom f & y = f.x by FUNCT_1:def 5;
         reconsider x as Element of LR by A24;
         consider a being Element of L such that
     A25: x = Class(ER, a) by A17;
           f.x = k.a by A15,A25;
       hence y in rngk by A5,A24,FUNCT_1:def 5;
      end;
      assume y in rngk; then consider x being set such that
     A26: x in dom k & y = k.x by FUNCT_1:def 5;
         reconsider x as Element of L by A26;
     A27: Class(ER, x) in CER by EQREL_1:def 5;
           f.Class(ER, x) = k.x by A15;
      hence y in rng f by A14,A26,A27,FUNCT_1:def 5;
     end;
then A28:  rng f = rngk by TARSKI:2;

       for x, y being Element of LR holds x <= y iff f.x <= f.y proof
      let x, y be Element of LR;
         x in CER by A7; then consider a being set such that
    A29: a in cL & x = Class(ER, a) by EQREL_1:def 5;
       reconsider a as Element of L by A29;
         y in CER by A7; then consider b being set such that
    A30: b in cL & y = Class(ER, b) by EQREL_1:def 5;
       reconsider b as Element of L by A30;
    A31: f.x = k.a & f.y = k.b by A15,A29,A30;
      hereby assume x <= y;
         then consider c, d being Element of L such that
      A32: x = Class(ER, c) & y = Class(ER, d) & k.c <= k.d by A8;
        f.x = k.c & f.y = k.d by A15,A32;
       hence f.x <= f.y by A32,YELLOW_0:61;
      end;
      assume f.x <= f.y;
       then k.a <= k.b by A31,YELLOW_0:60;
      hence x <= y by A8,A29,A30;
     end;
then A33: f is isomorphic by A22,A23,A28,WAYBEL_0:66;
      then LR, Image k are_isomorphic by WAYBEL_1:def 8;
then A34: Image k, LR are_isomorphic by WAYBEL_1:7;
A35: Image k is continuous LATTICE by A1,WAYBEL15:16;

    reconsider LR as non empty strict Poset by A34,Th15,Th16,Th17;
      Image k is complete by WAYBEL_1:57;
    then reconsider LR as complete (non empty strict Poset) by A34,Th18;
    reconsider LR as complete strict LATTICE;

    reconsider LR as continuous complete strict LATTICE by A34,A35,WAYBEL15:11;
   take LR;
   thus the carrier of LR = Class ER by A7;
      now let z be set;
     hereby assume
    A36: z in tIR; then consider a, b being set such that
    A37: a in CER & b in CER & z = [a, b] by A7,ZFMISC_1:def 2;
        reconsider a, b as Element of LR by A7,A37;
          a <= b by A36,A37,ORDERS_1:def 9;
        then consider x, y being Element of L such that
    A38: a = Class(ER, x) & b = Class(ER, y) & k.x <= k.y by A8;
      thus z in IR by A37,A38;
     end;
     assume z in IR; then consider x, y being Element of L such that
    A39: z = [Class(ER, x), Class(ER, y)] & k.x <= k.y;
           Class(ER, x) in CER by EQREL_1:def 5;
        then reconsider a = Class(ER, x) as Element of LR by A7;
           Class(ER, y) in CER by EQREL_1:def 5;
        then reconsider b = Class(ER, y) as Element of LR by A7;
          a <= b by A8,A39;
     hence z in tIR by A39,ORDERS_1:def 9;
    end;
   hence the InternalRel of LR = {[Class(ER, x), Class(ER, y)]
                  where x, y is Element of L : k.x <= k.y } by TARSKI:2;
   let g be map of L, LR such that
A40:  for x being Element of L holds g.x = Class(ER, x);
      (f qua Function)" is Function of the carrier of Image k, the carrier of
LR
       by A22,A23,A28,FUNCT_2:31;
    then reconsider f' = ((f qua Function)") as map of Image k, LR;
A41: f' is isomorphic by A33,WAYBEL_0:68;
      now let x be set; assume
    A42: x in cL;
        then reconsider x' = x as Element of L;
        A43: dom corestr k = cL by FUNCT_2:def 1;
    A44: f.Class(ER, x') = k.x' by A15;
        A45: Class(ER, x') in CER by EQREL_1:def 5;
     thus (f'*corestr k).x
        = f'.((corestr k).x) by A42,A43,FUNCT_1:23
       .= f'.(k.x) by WAYBEL_1:32
       .= Class(ER, x') by A14,A22,A44,A45,FUNCT_1:54
       .= g.x by A40;
    end;
then A46: g = f'*corestr k by FUNCT_2:18;
A47: corestr k is infs-preserving by WAYBEL_1:59;
A48: corestr k is directed-sups-preserving by A1,Th22;
A49: f' is infs-preserving by A41,WAYBEL13:20;
    reconsider f' as sups-preserving map of Image k, LR by A41,WAYBEL13:20;
A50: f' is directed-sups-preserving;
A51: g is infs-preserving by A46,A47,A49,Th26;
      g is directed-sups-preserving by A46,A48,A50,WAYBEL15:13;
  hence g is CLHomomorphism of L, LR by A51,WAYBEL16:def 1;
end;

theorem Th39: :: Theorem 2.11, p. 61-62, (2) implies (1)
    :: CCL: Immediate from 2.8. (?)  One has to construct a homomorphism.
 for L being continuous complete LATTICE, R being Subset of [:L, L:]
  st R is Equivalence_Relation of the carrier of L &
     ex LR being continuous complete LATTICE st
          the carrier of LR = Class EqRel R &
          for g being map of L, LR
           st for x being Element of L holds g.x = Class(EqRel R, x)
            holds g is CLHomomorphism of L, LR
   holds subrelstr R is CLSubFrame of [:L, L:]
proof let L be continuous complete LATTICE, R be Subset of [:L, L:] such that
A1: R is Equivalence_Relation of the carrier of L;
   given LR being continuous complete LATTICE such that
A2: the carrier of LR = Class EqRel R and
A3: for g being map of L, LR
    st for x being Element of L holds g.x = Class(EqRel R, x)
     holds g is CLHomomorphism of L, LR;
A4: EqRel R = R by A1,Def1;
   set cL = the carrier of L, cLR = the carrier of LR;
   set ER = EqRel R; set CER = Class ER;
   deffunc F(set) = Class(ER, $1);
A5: for x be set st x in cL holds F(x) in CER by EQREL_1:def 5;
   consider g being Function of cL, CER such that
A6: for x being set st x in cL holds g.x = F(x) from Lambda1(A5);
   reconsider g as map of L, LR by A2;
A7: for x being Element of L holds g.x = Class(EqRel R, x) by A6;
A8: dom g = cL by FUNCT_2:def 1;
A9: g is CLHomomorphism of L, LR by A3,A7;
   set k = g;
    now let x be set;
   hereby assume
  A10: x in R; then x in the carrier of [:L, L:];
      then x in [:cL, cL:] by YELLOW_3:def 2;
      then consider x1, x2 being set such that
  A11: x1 in cL & x2 in cL & x = [x1, x2] by ZFMISC_1:def 2;
      reconsider x1, x2 as Element of L by A11;
  A12: k.x1 = Class(EqRel R, x1) & k.x2 = Class(EqRel R, x2) by A6;
        x1 in Class(EqRel R, x2) by A4,A10,A11,EQREL_1:27;
      then k.x1 = k.x2 by A12,EQREL_1:31;
  then A13: [k.x1, k.x2] in id cLR by RELAT_1:def 10;
  A14: [:k, k:].[x1, x2] = [k.x1, k.x2] by A8,FUNCT_3:def 9;
        dom [:k, k:] = [:dom k, dom k:] by FUNCT_3:def 9;
      then [x1, x2] in dom [:k, k:] by A8,ZFMISC_1:106;
    hence x in [:k, k:]"(id cLR) by A11,A13,A14,FUNCT_1:def 13;
   end;
   assume x in [:k, k:]"(id cLR);
  then A15: x in dom [:k, k:] & [:k, k:].x in id cLR by FUNCT_1:def 13;
      then x in [:dom k, dom k:] by FUNCT_3:def 9;
      then consider x1, x2 being set such that
  A16: x1 in dom k & x2 in dom k & x = [x1, x2] by ZFMISC_1:def 2;
      reconsider x1, x2 as Element of L by A16;
        [:k, k:].[x1, x2] = [k.x1, k.x2] by A16,FUNCT_3:def 9;
  then A17: k.x1 = k.x2 by A15,A16,RELAT_1:def 10;
        k.x1=Class(EqRel R, x1) & k.x2 = Class(EqRel R, x2) by A6;
      then x1 in Class(ER, x2) by A17,EQREL_1:31;
   hence x in R by A4,A16,EQREL_1:27;
  end;
 then R = [:g, g:]"(id the carrier of LR) by TARSKI:2;
 hence subrelstr R is CLSubFrame of [:L, L:] by A9,Th35;
end;

definition
 let L be non empty reflexive RelStr;
 cluster directed-sups-preserving kernel map of L, L;
 existence proof
  reconsider k = id L as directed-sups-preserving kernel map of L, L;
  take k;
  thus thesis;
 end;
end;

definition
 let L be non empty reflexive RelStr, k be kernel map of L, L;
 func kernel_congruence k -> non empty Subset of [:L, L:] equals
:Def4: [:k, k:]"(id the carrier of L);
 coherence proof
  set cL = the carrier of L;
A1: dom k = cL by FUNCT_2:def 1;
   consider x being Element of cL;
   dom [:k, k:] = [:dom k, dom k:] by FUNCT_3:def 9;
then A2: [x, x] in dom [:k, k:] by A1,ZFMISC_1:def 2;
A3: [k.x, k.x] in id cL by RELAT_1:def 10;
     [:k, k:].[x,x] = [k.x, k.x] by A1,FUNCT_3:def 9;
  hence thesis by A2,A3,FUNCT_1:def 13;
 end;
end;

theorem Th40:
 for L being non empty reflexive RelStr, k being kernel map of L, L
  holds kernel_congruence k is Equivalence_Relation of the carrier of L
proof
 let L be non empty reflexive RelStr, k be kernel map of L, L;
 set R = kernel_congruence k;
   R = [:k, k:]"(id the carrier of L) by Def4;
 hence R is Equivalence_Relation of the carrier of L by Th2;
end;

theorem Th41: :: Theorem 2.11, p. 61-62 (3) implies (1)
               :: Not in CCL, consequence of other implications.
 for L being continuous complete LATTICE,
     k being directed-sups-preserving kernel map of L, L
  holds kernel_congruence k is CLCongruence
proof let L be continuous complete LATTICE,
          k be directed-sups-preserving kernel map of L, L;
 set R = kernel_congruence k;
 thus
A1: R is Equivalence_Relation of the carrier of L by Th40;
   R = [:k, k:]"(id the carrier of L) by Def4;
   then consider LR being continuous complete strict LATTICE such that
A2: the carrier of LR = Class EqRel R and
       the InternalRel of LR = {[Class(EqRel R, x), Class(EqRel R, y)]
                             where x, y is Element of L : k.x <= k.y } and
A3: for g being map of L, LR
      st for x being Element of L holds g.x = Class(EqRel R, x)
       holds g is CLHomomorphism of L, LR by Th38;
 thus subrelstr R is CLSubFrame of [:L, L:] by A1,A2,A3,Th39;
end;

definition :: Definition 2.12, p. 62, part II (lattice quotient)
 let L be continuous complete LATTICE,
     R be non empty Subset of [:L, L:] such that
A1: R is CLCongruence;
 func L ./. R -> continuous complete strict LATTICE means :Def5:
  the carrier of it = Class EqRel R &
  for x, y being Element of it holds x <= y iff "/\"(x, L) <= "/\"(y, L);
 existence proof set k = kernel_op R;
    k is directed-sups-preserving &
  R = [:k, k:]"(id the carrier of L) by A1,Th37;
  then consider LR being continuous complete strict LATTICE such that
A2: the carrier of LR = Class EqRel R and
A3: the InternalRel of LR = {[Class(EqRel R, x), Class(EqRel R, y)]
                            where x, y is Element of L : k.x <= k.y } and
     for g being map of L, LR
     st for x being Element of L holds g.x = Class(EqRel R, x)
    holds g is CLHomomorphism of L, LR by Th38;
   take LR;
   thus the carrier of LR = Class EqRel R by A2;
   let x, y be Element of LR;
A4: x in the carrier of LR & y in the carrier of LR;
   then consider u being set such that
A5: u in the carrier of L & x = Class(EqRel R, u) by A2,EQREL_1:def 5;
   consider v being set such that
A6: v in the carrier of L & y = Class(EqRel R, v) by A2,A4,EQREL_1:def 5;
   reconsider u, v as Element of L by A5,A6;
A7: k.u = inf Class(EqRel R, u) & k.v = inf Class(EqRel R, v) by A1,Def3;
   hereby assume x <= y;
     then [x, y] in the InternalRel of LR by ORDERS_1:def 9;
     then consider u', v' being Element of L such that
A8:   [x, y] = [Class(EqRel R, u'), Class(EqRel R, v')] & k.u' <= k.v' by A3;
A9:   x = Class(EqRel R, u') & y = Class(EqRel R, v') by A8,ZFMISC_1:33;
       k.u' = inf Class(EqRel R, u') & k.v' = inf Class(EqRel R, v') by A1,Def3
;
    hence "/\"(x, L) <= "/\"(y, L) by A8,A9;
   end;
   assume "/\"(x, L) <= "/\"(y, L);
    then [x, y] in the InternalRel of LR by A3,A5,A6,A7;
   hence x <= y by ORDERS_1:def 9;
 end;
 uniqueness proof
   let LR1, LR2 be continuous complete strict LATTICE such that
A10: the carrier of LR1 = Class EqRel R and
A11: for x, y being Element of LR1 holds x <= y iff "/\"(x, L) <= "/\"(y, L)and
A12: the carrier of LR2 = Class EqRel R and
A13: for x, y being Element of LR2 holds x <= y iff "/\"(x, L) <= "/\"(y, L);
    set cLR1 = the carrier of LR1; set cLR2 = the carrier of LR2;
      now let z be set;
     hereby assume
     A14: z in the InternalRel of LR1;
       then consider x, y being set such that
     A15: x in cLR1 & y in cLR1 & z = [x, y] by ZFMISC_1:def 2;
       reconsider x, y as Element of LR1 by A15;
       reconsider x' = x, y' = y as Element of LR2 by A10,A12;
         x <= y by A14,A15,ORDERS_1:def 9;
       then "/\"(x, L) <= "/\"(y, L) by A11;
       then x' <= y' by A13;
      hence z in the InternalRel of LR2 by A15,ORDERS_1:def 9;
     end;
     assume
     A16: z in the InternalRel of LR2;
       then consider x, y being set such that
     A17: x in cLR2 & y in cLR2 & z = [x, y] by ZFMISC_1:def 2;
       reconsider x, y as Element of LR2 by A17;
       reconsider x' = x, y' = y as Element of LR1 by A10,A12;
         x <= y by A16,A17,ORDERS_1:def 9;
       then "/\"(x, L) <= "/\"(y, L) by A13;
       then x' <= y' by A11;
      hence z in the InternalRel of LR1 by A17,ORDERS_1:def 9;
    end;
   hence LR1 = LR2 by A10,A12,TARSKI:2;
 end;
end;

theorem
  for L being continuous complete LATTICE, R being non empty Subset of [:L, L:]
 st R is CLCongruence
  for x being set holds
    x is Element of L./.R iff ex y being Element of L st x = Class(EqRel R, y)
proof let L be continuous complete LATTICE,
          R be non empty Subset of [:L, L:]; assume
   R is CLCongruence;
then A1: the carrier of (L./.R) = Class EqRel R by Def5;
 let x be set;
 hereby assume x is Element of L./.R;
   then x in Class EqRel R by A1;
   then consider y being set such that
 A2: y in the carrier of L & x = Class(EqRel R, y) by EQREL_1:def 5;
   reconsider y as Element of L by A2;
   take y;
   thus x = Class(EqRel R, y) by A2;
 end;
 given y being Element of L such that
A3: x = Class(EqRel R, y);
     x in Class EqRel R by A3,EQREL_1:def 5;
 hence x is Element of L./.R by A1;
end;

theorem :: Corollary 2.13, p. 62, (congruence --> kernel --> congruence)
   for L being continuous complete LATTICE,
     R being non empty Subset of [:L, L:]
  st R is CLCongruence
   holds R = kernel_congruence kernel_op R
proof let L be continuous complete LATTICE,
      R be non empty Subset of [:L, L:] such that
A1: R is CLCongruence;
    set cL = the carrier of L, km = kernel_op R;
  R = [:km, km:]"(id cL) by A1,Th37;
 hence R = kernel_congruence kernel_op R by Def4;
end;

theorem :: Corollary 2.13, p. 62, (kernel --> congruence --> kernel)
   for L being continuous complete LATTICE,
     k being directed-sups-preserving kernel map of L, L
   holds k = kernel_op kernel_congruence k
proof let L be continuous complete LATTICE,
          k be directed-sups-preserving kernel map of L, L;
 set kc = kernel_congruence k, cL = the carrier of L,
     km = kernel_op kc;
A1: kc is CLCongruence by Th41;
then A2: kc = [:km, km:]"(id cL) by Th37;
A3: kc = [:k, k:]"(id cL) by Def4;
A4: dom k = cL & dom km = cL by FUNCT_2:def 1;
A5: dom [:k, k:] = [:dom k, dom k:] by FUNCT_3:def 9;
A6: dom [:km, km:] = [:dom km, dom km:] by FUNCT_3:def 9;
A7: k <= id L & km <= id L by WAYBEL_1:def 15;
    reconsider kc' = kc as Equivalence_Relation of cL by A1,Def2;
    field kc' = cL by ORDERS_1:97;
    then
A8: kc' is_transitive_in cL by RELAT_2:def 16;
    now let x be set; assume
    x in cL;
     then reconsider x' = x as Element of L;
 A9: k.(k.x') = (k*k).x' by A4,FUNCT_1:23
              .= k.x' by QUANTAL1:def 9;
 A10: [k.x', k.x'] in id cL by RELAT_1:def 10;
 A11: [:k, k:].[k.x', x'] = [k.(k.x'), k.x'] by A4,FUNCT_3:def 9;
       [k.x', x'] in dom [:k, k:] by A4,A5,ZFMISC_1:def 2;
 then A12: [k.x', x'] in kc by A3,A9,A10,A11,FUNCT_1:def 13;
 A13: km.(km.x') = (km*km).x' by A4,FUNCT_1:23
                .= km.x' by QUANTAL1:def 9;
 A14: [km.x', km.x'] in id cL by RELAT_1:def 10;
 A15: [:km, km:].[x', km.x'] = [km.x', km.(km.x')] by A4,FUNCT_3:def 9;
        [x', km.x'] in dom [:km, km:] by A4,A6,ZFMISC_1:def 2;
      then [x', km.x'] in kc by A2,A13,A14,A15,FUNCT_1:def 13;
 then A16: [k.x', km.x'] in kc by A8,A12,RELAT_2:def 8;
     then [k.x', km.x'] in dom [:k, k:] &
     [:k, k:].[k.x', km.x'] in id cL by A3,FUNCT_1:def 13;
     then [k.(k.x'), k.(km.x')] in id cL by A4,FUNCT_3:def 9;
 then A17: k.(km.x') = k.(k.x') by RELAT_1:def 10
              .= (k*k).x' by A4,FUNCT_1:23
              .= k.x' by QUANTAL1:def 9;
       k.(km.x') <= (id L).(km.x') by A7,YELLOW_2:10;
 then A18: k.(km.x') <= km.x' by GRCAT_1:11;
       [k.x', km.x'] in dom [:km, km:] &
     [:km, km:].[k.x', km.x'] in id cL by A2,A16,FUNCT_1:def 13;
     then [km.(k.x'), km.(km.x')] in id cL by A4,FUNCT_3:def 9;
 then A19: km.(k.x') = km.(km.x') by RELAT_1:def 10
              .= (km*km).x' by A4,FUNCT_1:23
              .= km.x' by QUANTAL1:def 9;
       km.(k.x') <= (id L).(k.x') by A7,YELLOW_2:10;
     then km.(k.x') <= k.x' by GRCAT_1:11;
   hence k.x = km.x by A17,A18,A19,YELLOW_0:def 3;
  end;
 hence k = kernel_op kernel_congruence k by FUNCT_2:18;
end;

:: Theorem 2.14, p. 63, see WAYBEL15:17

theorem :: Proposition 2.15, p. 63
        :: That Image p is infs-inheriting follows from O-3.11 (iii)
   for L being continuous complete LATTICE,
     p being projection map of L, L
  st p is infs-preserving
   holds Image p is continuous LATTICE & Image p is infs-inheriting
proof let L be continuous complete LATTICE,
          p be projection map of L, L such that
A1: p is infs-preserving;
   reconsider Lc = {c where c is Element of L: c <= p.c}
                                  as non empty Subset of L by WAYBEL_1:46;
A2: subrelstr Lc is sups-inheriting SubRelStr of L by WAYBEL_1:52;
A3: subrelstr Lc is infs-inheriting by A1,WAYBEL_1:54;
then A4: subrelstr Lc is continuous LATTICE by A2,WAYBEL_5:28;
A5: subrelstr Lc is complete by A3,YELLOW_2:32;
   reconsider pc = p|Lc as map of subrelstr Lc, subrelstr Lc by WAYBEL_1:48;
A6: pc is closure by WAYBEL_1:50;
A7: subrelstr rng pc is full SubRelStr of L by WAYBEL15:1;
A8: the carrier of subrelstr rng p = rng p by YELLOW_0:def 15
       .= rng pc by WAYBEL_1:47
       .= the carrier of subrelstr rng pc by YELLOW_0:def 15;
A9: Image p = subrelstr rng p by YELLOW_2:def 2
          .= subrelstr rng pc by A7,A8,YELLOW_0:58
          .= Image pc by YELLOW_2:def 2;
   reconsider cpc = corestr pc as map of subrelstr Lc, Image pc;
     pc is infs-preserving proof
    let X be Subset of subrelstr Lc; assume ex_inf_of X, subrelstr Lc;
    thus ex_inf_of pc.:X, subrelstr Lc by A5,YELLOW_0:17;
        the carrier of subrelstr Lc = Lc by YELLOW_0:def 15;
      then X c= the carrier of L by XBOOLE_1:1;
     then reconsider X' = X as Subset of L;
   A10: dom pc = the carrier of subrelstr Lc by FUNCT_2:def 1;
   A11: ex_inf_of X, L by YELLOW_0:17;
       then "/\"(X',L) in the carrier of subrelstr Lc by A3,YELLOW_0:def 18;
   then A12: inf X' = inf X by A11,YELLOW_0:64;
   A13: ex_inf_of X', L by YELLOW_0:17;
   A14: p preserves_inf_of X' by A1,WAYBEL_0:def 32;
   A15: ex_inf_of p.:X, L by YELLOW_0:17;
     ex_inf_of pc.:X,L by YELLOW_0:17;
   then A16: "/\"(pc.:X,L) in the carrier of subrelstr Lc by A3,YELLOW_0:def 18
;
         X c= the carrier of subrelstr Lc;
       then X c= Lc by YELLOW_0:def 15;
       then pc.:X = p.:X by EXTENS_1:1;
   hence inf (pc.:X)
       = inf (p.:X) by A15,A16,YELLOW_0:64
      .= p.inf X' by A13,A14,WAYBEL_0:def 30
      .= pc.inf X by A10,A12,FUNCT_1:70;
   end;
then A17: cpc is infs-preserving by Th19;
A18: cpc is sups-preserving by A6,WAYBEL_1:58;
  cpc is directed-sups-preserving proof
    let X be Subset of subrelstr Lc such that X is non empty directed;
    thus cpc preserves_sup_of X by A18,WAYBEL_0:def 33;
   end;
 hence Image p is continuous LATTICE by A4,A5,A9,A17,WAYBEL_5:33;
 thus Image p is infs-inheriting by A1,A3,WAYBEL_1:54;
end;

Back to top