The Mizar article:

Auxiliary and Approximating Relations

by
Adam Grabowski

Received October 21, 1996

Copyright (c) 1996 Association of Mizar Users

MML identifier: WAYBEL_4
[ MML identifier index ]


environ

 vocabulary RELAT_2, ORDERS_1, RELAT_1, WAYBEL_3, LATTICES, LATTICE3, WAYBEL_0,
      BOOLE, YELLOW_1, SETFAM_1, BHSP_3, YELLOW_0, QUANTAL1, PRE_TOPC, FUNCT_1,
      FILTER_2, SEQM_3, PARTFUN1, CAT_1, GROUP_1, FUNCOP_1, FUNCT_2, CARD_3,
      RLVECT_2, WELLORD1, YELLOW_2, FILTER_0, WELLORD2, ORDINAL2, WAYBEL_2,
      SUBSET_1, ORDERS_2, WAYBEL_4;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, STRUCT_0, ORDERS_1,
      PRE_TOPC, PARTFUN1, LATTICE3, RELAT_1, RELAT_2, RELSET_1, FUNCT_1,
      FUNCT_2, WELLORD1, YELLOW_0, PRE_CIRC, CARD_3, PRALG_1, YELLOW_1, ALG_1,
      YELLOW_2, YELLOW_4, WAYBEL_0, WAYBEL_1, WAYBEL_2, WAYBEL_3;
 constructors ORDERS_3, PRE_CIRC, TOLER_1, WAYBEL_1, WAYBEL_2, WAYBEL_3,
      YELLOW_4, ALG_1;
 clusters LATTICE3, RELSET_1, STRUCT_0, WAYBEL_0, WAYBEL_2, WAYBEL_3, YELLOW_1,
      YELLOW_2, SUBSET_1, PARTFUN1, XBOOLE_0;
 requirements SUBSET, BOOLE;
 definitions LATTICE3, XBOOLE_0, TARSKI, YELLOW_0, WAYBEL_0, RELAT_1, YELLOW_2,
      ORDERS_3;
 theorems FUNCOP_1, FUNCT_1, FUNCT_2, LATTICE3, ORDERS_1, ORDERS_3, PARTFUN1,
      PRE_TOPC, RELAT_1, RELAT_2, RELSET_1, SETFAM_1, STRUCT_0, TARSKI,
      WAYBEL_0, WAYBEL_3, WAYBEL_2, WELLORD1, WELLORD2, YELLOW_0, YELLOW_1,
      YELLOW_2, YELLOW_4, ZFMISC_1, XBOOLE_0, XBOOLE_1;
 schemes FUNCT_2, PARTFUN1, RELSET_1, YELLOW_2, XBOOLE_0;

begin :: Auxiliary Relations

definition
 let L be non empty reflexive RelStr;
 canceled;

 func L-waybelow -> Relation of L means :Def2:
  for x,y being Element of L holds [x,y] in it iff x << y;
 existence
 proof
  defpred P[set,set] means
    ex x', y' be Element of L st x' = $1 & y' = $2 & x' << y';
  consider R being Relation of the carrier of L, the carrier of L such that
A1: for x,y being set holds [x,y] in R iff x in the carrier of L &
    y in the carrier of L & P[x,y] from Rel_On_Set_Ex;
  reconsider R as Relation of L ;
  take R;
  let x,y be Element of L;
  hereby assume [x,y] in R;
   then consider x', y' being Element of L such that
A2:   x' = x & y' = y & x' << y' by A1;
   thus x << y by A2;
  end;
  assume x << y;
  hence [x,y] in R by A1;
 end;
 uniqueness
 proof
  let A1,A2 be Relation of L;
  assume A3: for x,y being Element of L holds [x,y] in A1 iff x << y;
  assume A4: for x,y being Element of L holds [x,y] in A2 iff x << y;
  thus A1 = A2
  proof
   let a,b be set;
   hereby assume A5: [a,b] in A1;
    then a in the carrier of L & b in the carrier of L by ZFMISC_1:106;
    then reconsider a' = a, b' = b as Element of L;
      a' << b' by A3,A5;
    hence [a,b] in A2 by A4;
   end;
   assume A6: [a,b] in A2;
   then a in the carrier of L & b in the carrier of L by ZFMISC_1:106;
   then reconsider a' = a, b' = b as Element of L;
     a' << b' by A4,A6;
   hence [a,b] in A1 by A3;
  end;
 end;
end;

definition let L be RelStr;
  func IntRel L -> Relation of L equals :Def3:
    the InternalRel of L;
  coherence ;
  correctness;
end;

Lm1:
 for L being RelStr, x, y being Element of L holds
  [x, y] in IntRel L iff x <= y
  proof
   let L be RelStr, x, y be Element of L;
   hereby assume [x, y] in IntRel L;
    then [x, y] in the InternalRel of L by Def3;
    hence x <= y by ORDERS_1:def 9;
   end;
   assume x <= y;
   then [x, y] in the InternalRel of L by ORDERS_1:def 9;
   hence [x, y] in IntRel L by Def3;
  end;

definition let L be RelStr, R be Relation of L;
  attr R is auxiliary(i) means :Def4:
   for x, y being Element of L holds
    [x,y] in R implies x <= y;

  attr R is auxiliary(ii) means :Def5:
   for x, y, z, u being Element of L holds
    ( u <= x & [x,y] in R & y <= z implies [u,z] in R );
end;

definition let L be non empty RelStr, R be Relation of L;
  attr R is auxiliary(iii) means :Def6:
   for x, y, z being Element of L holds
   ( [x,z] in R & [y,z] in R implies [(x "\/" y),z] in R );

  attr R is auxiliary(iv) means :Def7:
   for x being Element of L holds [Bottom L,x] in R;
end;

:: Definition 1.9 p.43
definition let L be non empty RelStr, R be Relation of L;
  attr R is auxiliary means :Def8:
   R is auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv);
end;

definition let L be non empty RelStr;
  cluster auxiliary ->
    auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) Relation of L;
  coherence by Def8;
  cluster auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) ->
    auxiliary Relation of L;
  coherence by Def8;
end;

definition let L be lower-bounded with_suprema transitive antisymmetric RelStr;
 cluster auxiliary Relation of L;
 existence
  proof
    set A = IntRel L;
    take A;
    thus A is auxiliary(i)
    proof
      let x, y be Element of L;
      assume [x,y] in A;
      then [x,y] in the InternalRel of L by Def3;
      hence thesis by ORDERS_1:def 9;
    end;
    thus A is auxiliary(ii)
    proof
      let x, y, z, u be Element of L;
      assume that
A1:   u <= x and
A2:   [x,y] in A and
A3:   y <= z;
        [x,y] in the InternalRel of L by A2,Def3;
      then x <= y by ORDERS_1:def 9;
      then u <= y by A1,ORDERS_1:26;
      then u <= z by A3,ORDERS_1:26;
      then [u,z] in the InternalRel of L by ORDERS_1:def 9;
      hence thesis by Def3;
    end;
    thus A is auxiliary(iii)
    proof
      let x, y, z be Element of L;
      assume that A4: [x,z] in A and A5: [y,z] in A;
        [x,z] in the InternalRel of L by A4,Def3;
then A6:   x <= z by ORDERS_1:def 9;
        [y,z] in the InternalRel of L by A5,Def3;
then A7:   y <= z by ORDERS_1:def 9;
        ex q being Element of L st x <= q & y <= q &
       for c being Element of L st x <= c & y <= c holds q <= c
        by LATTICE3:def 10;
      then (x "\/" y) <= z by A6,A7,LATTICE3:def 13;
      then [x "\/" y, z] in the InternalRel of L by ORDERS_1:def 9;
      hence thesis by Def3;
    end;
    thus A is auxiliary(iv)
    proof
     let x be Element of L;
       Bottom L <= x by YELLOW_0:44;
     then [Bottom L,x] in the InternalRel of L by ORDERS_1:def 9;
     hence thesis by Def3;
    end;
  end;
end;

theorem Th1:
 for L being lower-bounded sup-Semilattice
  for AR being auxiliary(ii) auxiliary(iii) Relation of L
   for x, y, z, u being Element of L holds
   [x, z] in AR & [y, u] in AR implies [x "\/" y, z "\/" u] in AR
  proof
  let L be lower-bounded sup-Semilattice;
  let AR be auxiliary(ii) auxiliary(iii) Relation of L;
  let x,y,z,u be Element of L;
   assume
A1: [x, z] in AR & [y, u] in AR;
A2: x <= x & y <= y;
      z <= z "\/" u & u <= z "\/" u by YELLOW_0:22;
    then [x, z "\/" u] in AR & [y, z "\/" u] in AR by A1,A2,Def5;
    hence [x "\/" y, z "\/" u] in AR by Def6;
  end;

Lm2:
  for L be lower-bounded sup-Semilattice
   for AR be auxiliary(i) auxiliary(ii) Relation of L holds
    AR is transitive
  proof
   let L be lower-bounded sup-Semilattice;
   let AR be auxiliary(i) auxiliary(ii) Relation of L;
A1:  field AR c= (the carrier of L) \/ (the carrier of L) by RELSET_1:19;
      now let x,y,z be set;
      assume
A2:    x in field AR & y in field AR & z in field AR & [x,y] in AR & [y,z] in
 AR;
      then reconsider x'=x, y'=y, z'=z as Element of L by A1;
      reconsider x', y', z' as Element of L;
A3:    x' <= y' by A2,Def4;
        z' <= z';
      hence [x,z] in AR by A2,A3,Def5;
    end;
    then AR is_transitive_in field AR by RELAT_2:def 8;
    hence thesis by RELAT_2:def 16;
  end;

definition let L be lower-bounded sup-Semilattice;
  cluster auxiliary(i) auxiliary(ii) -> transitive Relation of L;
  coherence by Lm2;
end;

definition let L be RelStr;
  cluster IntRel L -> auxiliary(i);
  coherence
  proof
   let x, y be Element of L;
   assume [x, y] in IntRel L;
   hence x <= y by Lm1;
 end;
end;

definition let L be transitive RelStr;
  cluster IntRel L -> auxiliary(ii);
  coherence
  proof
   set A = IntRel L;
     let x,y,z,u be Element of L;
     assume that A1: u <= x and A2: [x,y] in A and A3: y <= z;
       x <= y by A2,Lm1;
     then u <= y by A1,ORDERS_1:26;
     then u <= z by A3,ORDERS_1:26;
     hence [u,z] in A by Lm1;
   end;
 end;

definition let L be with_suprema antisymmetric RelStr;
  cluster IntRel L -> auxiliary(iii);
  coherence
  proof
   set A = IntRel L;
     let x,y,z be Element of L;
     assume that A1: [x,z] in A and A2: [y,z] in A;
A3:  x <= z by A1,Lm1;
A4:  y <= z by A2,Lm1;
       ex q being Element of L st x <= q & y <= q &
       for c being Element of L st x <= c & y <= c holds q <= c
        by LATTICE3:def 10;
     then x "\/" y <= z by A3,A4,LATTICE3:def 13;
     hence thesis by Lm1;
   end;
 end;

definition let L be lower-bounded antisymmetric non empty RelStr;
  cluster IntRel L -> auxiliary(iv);
  coherence
  proof
   set A = IntRel L;
     for x be Element of L holds [Bottom L,x] in A
   proof
     let x be Element of L;
       Bottom L <= x by YELLOW_0:44;
     hence thesis by Lm1;
   end;
   hence A is auxiliary(iv) by Def7;
  end;
end;

 reserve a for set;

definition let L be lower-bounded sup-Semilattice;
  func Aux L means :Def9:
   a in it iff a is auxiliary Relation of L;
   existence
   proof defpred P[set] means $1 is auxiliary Relation of L;
     consider X be set such that
A1:    for a holds a in X
       iff a in bool [:the carrier of L,the carrier of L:] & P[a]
         from Separation;
     take X;
     thus thesis by A1;
   end;
   uniqueness
   proof
     let A1,A2 be set such that
A2:   a in A1 iff a is auxiliary Relation of L and
A3:   a in A2 iff a is auxiliary Relation of L;
     thus A1 = A2
     proof
       thus A1 c= A2
       proof
         let a; assume a in A1;
         then a is auxiliary Relation of L by A2;
         hence thesis by A3;
       end;
       let a; assume a in A2;
       then a is auxiliary Relation of L by A3;
       hence thesis by A2;
     end;
   end;
end;

definition let L be lower-bounded sup-Semilattice;
  cluster Aux L -> non empty;
  coherence
  proof
      IntRel L is auxiliary Relation of L;
    hence thesis by Def9;
  end;
end;

Lm3:
 for L being lower-bounded sup-Semilattice
  for AR being auxiliary(i) Relation of L
   for a,b being set st [a,b] in AR holds [a,b] in IntRel L
 proof
  let L be lower-bounded sup-Semilattice;
  let AR be auxiliary(i) Relation of L;
  let a,b be set; assume A1: [a,b] in AR;
  then a in the carrier of L & b in the carrier of L by ZFMISC_1:106;
  then reconsider a' = a, b' = b as Element of L;
    a' <= b' by A1,Def4;
  hence thesis by Lm1;
 end;

theorem Th2:
 for L being lower-bounded sup-Semilattice
  for AR being auxiliary(i) Relation of L holds
   AR c= IntRel L
 proof
  let L be lower-bounded sup-Semilattice;
  let AR be auxiliary(i) Relation of L;
  let a,b be set; assume [a,b] in AR;
  hence thesis by Lm3;
 end;

theorem
   for L being lower-bounded sup-Semilattice holds
  Top InclPoset Aux L = IntRel L
 proof
  let L be lower-bounded sup-Semilattice;
    IntRel L = "/\"({},InclPoset Aux L)
  proof
   set P = InclPoset Aux L;
   set I = IntRel L;
     I in Aux L by Def9;
   then I in the carrier of P by YELLOW_1:1;
   then reconsider I as Element of P;
A1: I is_<=_than {} by YELLOW_0:6;
     for b being Element of P st b is_<=_than {} holds I >= b
   proof
    let b be Element of P;
      b in the carrier of InclPoset Aux L;
    then b in Aux L by YELLOW_1:1;
    then reconsider b' = b as auxiliary Relation of L by Def9;
    assume b is_<=_than {};
      b' c= I by Th2;
    hence thesis by YELLOW_1:3;
   end;
   hence thesis by A1,YELLOW_0:31;
  end;
  hence thesis by YELLOW_0:def 12;
 end;

definition let L be lower-bounded sup-Semilattice;
 cluster InclPoset Aux L -> upper-bounded;
 coherence
 proof
  set I = IntRel L;
    I in Aux L by Def9;
  then I in the carrier of InclPoset Aux L by YELLOW_1:1;
  then reconsider I as Element of InclPoset Aux L;
  take I;
    I is_>=_than the carrier of InclPoset Aux L
  proof
   let b be Element of InclPoset Aux L;
   assume b in the carrier of InclPoset Aux L;
   then b in Aux L by YELLOW_1:1;
   then reconsider b' = b as auxiliary Relation of L by Def9;
     b' c= I by Th2;
   hence thesis by YELLOW_1:3;
  end;
  hence thesis;
 end;
end;

definition let L be non empty RelStr;
 func AuxBottom L -> Relation of L means :Def10:
  for x,y be Element of L holds [x,y] in it iff x = Bottom L;
 existence
 proof defpred P[set,set] means $1 = Bottom L;
  consider R being Relation of the carrier of L, the carrier of L such that
A1: for a,b be set holds [a,b] in R iff a in the carrier of L &
       b in the carrier of L & P[a,b] from Rel_On_Set_Ex;
  reconsider R as Relation of L ;
  take R;
  let x,y be Element of L;
  thus [x,y] in R implies x = Bottom L by A1;
  assume x = Bottom L;
  hence [x,y] in R by A1;
 end;
 uniqueness
 proof
  let A1,A2 be Relation of L;
  assume A2: for x,y be Element of L holds [x,y] in A1 iff x = Bottom L;
  assume A3: for x,y be Element of L holds [x,y] in A2 iff x = Bottom L;
  thus A1 = A2
  proof
   let a,b be set;
   hereby assume A4: [a,b] in A1;
    then a in the carrier of L & b in the carrier of L by ZFMISC_1:106;
    then reconsider a' = a, b' = b as Element of L;
      [a',b'] in A1 by A4;
    then a' = Bottom L by A2;
    then [a',b'] in A2 by A3;
    hence [a,b] in A2;
   end;
   assume A5: [a,b] in A2;
   then a in the carrier of L & b in the carrier of L by ZFMISC_1:106;
   then reconsider a' = a, b' = b as Element of L;
     [a',b'] in A2 by A5;
   then a' = Bottom L by A3;
   then [a',b'] in A1 by A2;
   hence [a,b] in A1;
  end;
 end;
end;

definition let L be lower-bounded sup-Semilattice;
 cluster AuxBottom L -> auxiliary;
 coherence
 proof
  set A = AuxBottom L;
A1:A is auxiliary(i)
  proof
   let x, y be Element of L;
   assume [x,y] in A;
   then x = Bottom L by Def10;
   hence thesis by YELLOW_0:44;
  end;
A2:A is auxiliary(ii)
  proof let x, y, z, u be Element of L;
   assume A3: u <= x & [x,y] in A & y <= z;
then A4: x = Bottom L by Def10;
     Bottom L <= u by YELLOW_0:44;
   then u = Bottom L by A3,A4,ORDERS_1:25;
   hence thesis by Def10;
  end;
A5:A is auxiliary(iii)
  proof
   let x, y, z be Element of L;
   assume [x,z] in A & [y,z] in A;
then A6: x = Bottom L & y = Bottom L by Def10;
   then x <= y;
   then x "\/" y = Bottom L by A6,YELLOW_0:24;
   hence thesis by Def10;
  end;
    for x be Element of L holds [Bottom L,x] in A by Def10;
  then A is auxiliary(iv) by Def7;
  hence thesis by A1,A2,A5,Def8;
 end;
end;

theorem Th4:
 for L being lower-bounded sup-Semilattice
  for AR being auxiliary(iv) Relation of L holds AuxBottom L c= AR
  proof
   let L be with_suprema lower-bounded Poset;
   let AR be auxiliary(iv) Relation of L;
   let a,b be set;
   assume A1: [a,b] in AuxBottom L;
   then a in the carrier of L & b in the carrier of L by ZFMISC_1:106;
   then reconsider a' = a, b' = b as Element of L;
     [a',b'] in AuxBottom L by A1;
   then a' = Bottom L by Def10;
   then [a',b'] in AR by Def7;
   hence [a,b] in AR;
  end;

theorem
   for L being lower-bounded sup-Semilattice
  for AR being auxiliary(iv) Relation of L holds
   Bottom InclPoset Aux L = AuxBottom L
 proof
  let L be with_suprema lower-bounded Poset;
  let AR be auxiliary(iv) Relation of L;
    AuxBottom L in Aux L by Def9;
  then AuxBottom L in the carrier of InclPoset Aux L by YELLOW_1:1;
  then reconsider N = AuxBottom L as Element of InclPoset Aux L;
    AuxBottom L = "\/"({},InclPoset Aux L)
  proof
A1: N is_>=_than {} by YELLOW_0:6;
     for b being Element of InclPoset Aux L st b is_>=_than {} holds N <= b
   proof
    let b be Element of InclPoset Aux L;
    assume b is_>=_than {};
      b in the carrier of InclPoset Aux L;
    then b in Aux L by YELLOW_1:1;
    then reconsider b' = b as auxiliary Relation of L by Def9;
      N c= b' by Th4;
    hence thesis by YELLOW_1:3;
   end;
   hence thesis by A1,YELLOW_0:30;
  end;
  hence thesis by YELLOW_0:def 11;
 end;

definition let L be lower-bounded sup-Semilattice;
 cluster InclPoset Aux L -> lower-bounded;
 coherence
 proof
  set I = AuxBottom L;
    I in Aux L by Def9;
  then I in the carrier of InclPoset Aux L by YELLOW_1:1;
  then reconsider I as Element of InclPoset Aux L;
  take I;
    I is_<=_than the carrier of InclPoset Aux L
  proof
   let b be Element of InclPoset Aux L;
   assume b in the carrier of InclPoset Aux L;
   then b in Aux L by YELLOW_1:1;
   then reconsider b' = b as auxiliary Relation of L by Def9;
     I c= b' by Th4;
   hence thesis by YELLOW_1:3;
  end;
  hence thesis;
 end;
end;

theorem Th6:
 for L being lower-bounded sup-Semilattice
  for a,b being auxiliary(i) Relation of L holds
    a /\ b is auxiliary(i) Relation of L
proof
 let L be with_suprema lower-bounded Poset;
 let a,b be auxiliary(i) Relation of L;
 reconsider ab = a /\ b as Relation of L ;
   for x, y be Element of L holds [x,y] in ab implies x <= y
 proof
  let x, y be Element of L;
  assume [x,y] in ab;
  then [x,y] in a & [x,y] in b by XBOOLE_0:def 3;
  hence x <= y by Def4;
 end;
 hence thesis by Def4;
end;

theorem Th7:
 for L being lower-bounded sup-Semilattice
  for a,b being auxiliary(ii) Relation of L holds
    a /\ b is auxiliary(ii) Relation of L
proof
 let L be with_suprema lower-bounded Poset;
 let a,b be auxiliary(ii) Relation of L;
 reconsider ab = a /\ b as Relation of L ;
   for x, y, z, u be Element of L holds
   u <= x & [x,y] in ab & y <= z implies [u,z] in ab
 proof
  let x, y, z, u be Element of L;
  assume A1: u <= x & [x,y] in ab & y <= z;
  then [x,y] in a & [x,y] in b by XBOOLE_0:def 3;
  then [u,z] in a & [u,z] in b by A1,Def5;
  hence thesis by XBOOLE_0:def 3;
 end;
 hence thesis by Def5;
end;

theorem Th8:
 for L being lower-bounded sup-Semilattice
  for a,b being auxiliary(iii) Relation of L holds
    a /\ b is auxiliary(iii) Relation of L
proof
 let L be with_suprema lower-bounded Poset;
 let a,b be auxiliary(iii) Relation of L;
 reconsider ab = a /\ b as Relation of L ;
   for x, y, z be Element of L holds
   [x,z] in ab & [y,z] in ab implies [(x "\/" y),z] in ab
 proof
  let x, y, z be Element of L;
  assume [x,z] in ab & [y,z] in ab;
  then [x,z] in a & [x,z] in b & [y,z] in a & [y,z] in b by XBOOLE_0:def 3;
  then [(x "\/" y),z] in a & [(x "\/" y),z] in b by Def6;
  hence thesis by XBOOLE_0:def 3;
 end;
 hence thesis by Def6;
end;

theorem Th9:
 for L being lower-bounded sup-Semilattice
  for a,b being auxiliary(iv) Relation of L holds
    a /\ b is auxiliary(iv) Relation of L
proof
 let L be with_suprema lower-bounded Poset;
 let a,b be auxiliary(iv) Relation of L;
 reconsider ab = a /\ b as Relation of L ;
   for x be Element of L holds [Bottom L,x] in ab
 proof
  let x be Element of L;
    [Bottom L,x] in a & [Bottom L,x] in b by Def7;
  hence thesis by XBOOLE_0:def 3;
 end;
 hence thesis by Def7;
end;

theorem Th10:
 for L being lower-bounded sup-Semilattice
  for a,b being auxiliary Relation of L holds
    a /\ b is auxiliary Relation of L
proof
 let L be with_suprema lower-bounded Poset;
 let a,b be auxiliary Relation of L;
 reconsider ab = a /\ b as Relation of L ;
   ab is auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv)
  by Th6,Th7,Th8,Th9;
 hence thesis by Def8;
end;

theorem Th11:
 for L being lower-bounded sup-Semilattice
  for X being non empty Subset of InclPoset Aux L holds
   meet X is auxiliary Relation of L
proof
 let L be with_suprema lower-bounded Poset;
 let X be non empty Subset of InclPoset Aux L;
   X c= the carrier of InclPoset Aux L;
then A1: X c= Aux L by YELLOW_1:1;
 consider a be Element of X;
   a in X;
 then a is auxiliary Relation of L by A1,Def9;
 then meet X c= [:the carrier of L,the carrier of L:] by SETFAM_1:8;
 then meet X is Relation of the carrier of L by RELSET_1:def 1;
 then reconsider ab = meet X as Relation of L ;
   now
 thus ab is auxiliary(i)
 proof
  let x, y be Element of L;
  assume A2: [x,y] in ab;
  consider V be Element of X;
A3: V in X;
A4: [x,y] in V by A2,SETFAM_1:def 1;
    V is auxiliary Relation of L by A1,A3,Def9;
  hence x <= y by A4,Def4;
 end;
 thus ab is auxiliary(ii)
 proof
  let x, y, z, u be Element of L;
  assume A5: u <= x & [x,y] in ab & y <= z;
    for Y be set st Y in X holds [u,z] in Y
  proof
   let Y be set; assume A6: Y in X;
then A7: Y is auxiliary Relation of L by A1,Def9;
     [x,y] in Y by A5,A6,SETFAM_1:def 1;
   hence thesis by A5,A7,Def5;
  end;
  hence thesis by SETFAM_1:def 1;
 end;
 thus ab is auxiliary(iii)
 proof
  let x, y, z be Element of L;
  assume A8: [x,z] in ab & [y,z] in ab;
    for Y be set st Y in X holds [(x "\/" y),z] in Y
  proof
   let Y be set; assume A9: Y in X;
then A10: Y is auxiliary Relation of L by A1,Def9;
     [x,z] in Y & [y,z] in Y by A8,A9,SETFAM_1:def 1;
   hence thesis by A10,Def6;
  end;
  hence thesis by SETFAM_1:def 1;
 end;
 thus ab is auxiliary(iv)
 proof
  let x be Element of L;
    for Y be set st Y in X holds [Bottom L,x] in Y
  proof
   let Y be set; assume Y in X;
 then Y is auxiliary Relation of L by A1,Def9;
   hence thesis by Def7;
  end;
  hence thesis by SETFAM_1:def 1;
 end;
 end;
 hence thesis by Def8;
end;

definition let L be lower-bounded sup-Semilattice;
 cluster InclPoset Aux L -> with_infima;
 coherence
  proof
     for x, y be set st (x in Aux L & y in Aux L) holds x /\ y in Aux L
   proof
    let x, y be set;
    assume x in Aux L & y in Aux L;
    then x is auxiliary Relation of L & y is auxiliary Relation of L by Def9;
    then x /\ y is auxiliary Relation of L by Th10;
    hence x /\ y in Aux L by Def9;
   end;
   hence InclPoset Aux L is with_infima by YELLOW_1:12;
  end;
end;

definition let L be lower-bounded sup-Semilattice;
 cluster InclPoset Aux L -> complete;
 coherence
 proof
    for X be Subset of InclPoset Aux L holds ex_inf_of X, InclPoset Aux L
  proof
   let X be Subset of InclPoset Aux L;
   set N = meet X;
   per cases;
   suppose A1: X <> {};
   then N is auxiliary Relation of L by Th11;
   then N in Aux L by Def9;
   then N in the carrier of InclPoset Aux L by YELLOW_1:1;
   then reconsider N as Element of InclPoset Aux L;
A2: X is_>=_than N
   proof
    let b be Element of InclPoset Aux L;
    assume b in X;
    then N c= b by SETFAM_1:4;
    hence N <= b by YELLOW_1:3;
   end;
     for b being Element of InclPoset Aux L st X is_>=_than b holds N >= b
   proof
    let b be Element of InclPoset Aux L;
    assume A3: X is_>=_than b;
      for Z1 be set st Z1 in X holds b c= Z1
    proof
     let Z1 be set; assume A4: Z1 in X;
     then reconsider Z1' = Z1 as Element of InclPoset Aux L;
       b <= Z1' by A3,A4,LATTICE3:def 8;
     hence b c= Z1 by YELLOW_1:3;
    end;
    then b c= meet X by A1,SETFAM_1:6;
    hence thesis by YELLOW_1:3;
   end;
   hence thesis by A2,YELLOW_0:16;
   suppose X = {};
   hence thesis by YELLOW_0:43;
  end;
  hence thesis by YELLOW_2:30;
 end;
end;

definition let L be non empty RelStr, x be Element of L;
  let AR be Relation of the carrier of L;
A1: {y where y is Element of L : [y,x] in AR} c= the carrier of L
 proof let z be set; assume z in {y where y is Element of L: [y,x] in AR};
   then ex y being Element of L st z = y & [y,x] in AR;
   hence thesis;
 end;
 func AR-below x -> Subset of L equals :Def11:
   {y where y is Element of L: [y,x] in AR};
 correctness by A1;

A2:  {y where y is Element of L: [x,y] in AR} c= the carrier of L
  proof let z be set; assume z in {y where y is Element of L: [x,y] in AR};
   then ex y being Element of L st z = y & [x,y] in AR;
   hence thesis;
  end;
 func AR-above x -> Subset of L equals :Def12:
   {y where y is Element of L: [x,y] in AR};
 correctness by A2;
end;

theorem Th12:
 for L being lower-bounded sup-Semilattice, x being Element of L
  for AR being auxiliary(i) Relation of L holds
   AR-below x c= downarrow x
 proof
   let L be lower-bounded sup-Semilattice, x be Element of L,
       AR be auxiliary(i) Relation of L;
   let a;
A1:AR-below x = {y where y is Element of L: [y,x] in AR} by Def11;
   assume a in AR-below x;
   then consider y1 be Element of L such that A2: y1 = a & [y1,x] in AR by A1;
     y1 <= x by A2,Def4;
   hence thesis by A2,WAYBEL_0:17;
 end;

definition let L be lower-bounded sup-Semilattice, x be Element of L;
  let AR be auxiliary(iv) Relation of L;
 cluster AR-below x -> non empty;
 coherence
 proof
   set I = AR-below x;
A1:I = {y where y is Element of L: [y,x] in AR} by Def11;
     [Bottom L,x] in AR by Def7;
   then Bottom L in I by A1;
   hence thesis;
 end;
end;

definition let L be lower-bounded sup-Semilattice, x be Element of L;
  let AR be auxiliary(ii) Relation of L;
 cluster AR-below x -> lower;
 coherence
 proof
   set I = AR-below x;
A1:I = {y where y is Element of L: [y,x] in AR} by Def11;
    let x1, y1 be Element of L;
    assume A2: x1 in I & y1 <= x1;
    then consider v1 be Element of L such that A3: v1 = x1 & [v1, x] in AR by
A1;
      x <= x;
    then [y1, x] in AR by A2,A3,Def5;
    hence thesis by A1;
 end;
end;

definition let L be lower-bounded sup-Semilattice, x be Element of L;
  let AR be auxiliary(iii) Relation of L;
 cluster AR-below x -> directed;
 coherence
 proof
   set I = AR-below x;
A1:I = {y where y is Element of L: [y,x] in AR} by Def11;
    let u1,u2 be Element of L; assume A2: u1 in I & u2 in I;
    then consider v1 be Element of L such that A3: v1 = u1 &
       [v1,x] in AR by A1;
    consider v2 be Element of L such that A4: v2 = u2 &
       [v2,x] in AR by A1,A2;
    take u12 = u1 "\/" u2;
      [u12,x] in AR by A3,A4,Def6;
    hence thesis by A1,YELLOW_0:22;
 end;
end;

definition let L be lower-bounded sup-Semilattice;
 let AR be auxiliary(ii) auxiliary(iii) auxiliary(iv) Relation of L;
 func AR-below -> map of L, InclPoset Ids L means :Def13:
  for x be Element of L holds
   it.x = AR-below x;
 existence
 proof
  deffunc F(Element of L) = AR-below $1;
A1:  for x being Element of L holds F(x) is Element of InclPoset Ids L
   proof
    let x be Element of L;
    reconsider I = F(x) as Ideal of L;
      I in {X where X is Ideal of L: not contradiction};
    then I in Ids L by WAYBEL_0:def 23;
    then I in the carrier of InclPoset Ids L by YELLOW_1:1;
    hence thesis;
   end;
  consider f being map of L, InclPoset Ids L such that
A2:  for x being Element of L holds f.x = F(x) from KappaMD(A1);
  take f;
  thus thesis by A2;
 end;
 uniqueness
 proof
  let M1, M2 be map of L, InclPoset Ids L;
  assume A3: for x be Element of L holds M1.x = AR-below x;
  assume A4: for x be Element of L holds M2.x = AR-below x;
    for x be set st x in the carrier of L holds M1.x = M2.x
  proof
   let x be set; assume x in the carrier of L;
   then reconsider x' = x as Element of L;
   thus M1.x = AR-below x' by A3
            .= M2.x by A4;
  end;
  hence thesis by FUNCT_2:18;
 end;
end;

theorem Th13:
 for L being non empty RelStr, AR being Relation of L
  for a being set, y being Element of L holds
   a in AR-below y iff [a,y] in AR
  proof
  let L be non empty RelStr, AR be Relation of L;
  let a be set, y be Element of L;
A1: AR-below y = {z where z is Element of L: [z,y] in AR} by Def11;
     a in AR-below y iff [a,y] in AR
   proof
    hereby assume a in AR-below y;
     then consider z being Element of L such that A2: a = z & [z,y] in AR by A1
;
     thus [a,y] in AR by A2;
    end;
    assume A3: [a,y] in AR;
    then a in the carrier of L by ZFMISC_1:106;
    then reconsider x' = a as Element of L;
      ex z being Element of L st a = z & [z,y] in AR
    proof
     take x';
     thus thesis by A3;
    end;
    hence a in AR-below y by A1;
   end;
   hence thesis;
  end;

theorem
   for L being sup-Semilattice, AR being Relation of L
  for y being Element of L holds
  a in AR-above y iff [y,a] in AR
proof
 let L be with_suprema Poset, AR be Relation of L;
 let y be Element of L;
A1: AR-above y = {z where z is Element of L: [y,z] in AR} by Def12;
     a in AR-above y iff [y,a] in AR
  proof
    hereby assume a in AR-above y;
     then consider z being Element of L such that A2: a = z & [y,z] in AR by A1
;
     thus [y,a] in AR by A2;
    end;
    assume A3: [y,a] in AR;
    then a in the carrier of L by ZFMISC_1:106;
    then reconsider x' = a as Element of L;
      ex z being Element of L st a = z & [y,z] in AR
   proof
     take x';
     thus thesis by A3;
    end;
    hence a in AR-above y by A1;
   end;
   hence thesis;
  end;

Lm4:
 for L be with_suprema lower-bounded Poset, AR be Relation of L
  for a be set, y be Element of L holds
   a in downarrow y iff [a,y] in the InternalRel of L
 proof
 let L be with_suprema lower-bounded Poset, AR be Relation of L;
 let a be set, y be Element of L;
  hereby assume A1: a in downarrow y;
   then reconsider a' = a as Element of L;
     a' <= y by A1,WAYBEL_0:17;
   hence [a,y] in the InternalRel of L by ORDERS_1:def 9;
  end;
  assume A2: [a,y] in the InternalRel of L;
  then a in the carrier of L by ZFMISC_1:106;
  then reconsider a' = a as Element of L;
    a' <= y by A2,ORDERS_1:def 9;
  hence thesis by WAYBEL_0:17;
 end;

theorem
   for L being lower-bounded sup-Semilattice, AR being auxiliary(i) Relation of
L
  for x being Element of L holds
   AR = the InternalRel of L implies AR-below x = downarrow x
 proof
  let L be lower-bounded sup-Semilattice, AR be auxiliary(i) Relation of L;
  let x be Element of L;
  assume A1: AR = the InternalRel of L;
  thus AR-below x c= downarrow x by Th12;
  thus downarrow x c= AR-below x
  proof
   let a; assume a in downarrow x;
   then [a,x] in AR by A1,Lm4;
   hence thesis by Th13;
  end;
 end;

definition let L be non empty Poset;
  func MonSet L -> strict RelStr means :Def14:
   ( a in the carrier of it iff
    ex s be map of L, InclPoset Ids L st a = s & s is monotone &
     for x be Element of L holds s.x c= downarrow x ) &
    for c, d be set holds [c,d] in the InternalRel of it iff
    ex f,g be map of L, InclPoset Ids L st c = f & d = g &
     c in the carrier of it & d in the carrier of it & f <= g;
  existence
  proof defpred P[set] means
    ex s be map of L, InclPoset Ids L st $1 = s &
     s is monotone &
     for x be Element of L holds s.x c= downarrow x;
   consider S be set such that
A1:  a in S iff a in PFuncs (the carrier of L, the carrier of
     InclPoset Ids L) & P[a] from Separation;
A2:  a in S iff
    ex s be map of L, InclPoset Ids L st a = s &
     s is monotone &
     for x be Element of L holds s.x c= downarrow x
   proof
    thus a in S implies
    ex s be map of L, InclPoset Ids L st a = s &
     s is monotone &
     for x be Element of L holds s.x c= downarrow x by A1;
    given s be map of L, InclPoset Ids L such that
A3:    a = s & s is monotone & for x be Element of L holds s.x c= downarrow x;
      s in PFuncs (the carrier of L, the carrier of
         InclPoset Ids L) by PARTFUN1:119;
    hence a in S by A1,A3;
   end;
   defpred P[set,set] means
     ex f,g be map of L, InclPoset Ids L st $1 = f & $2 = g & f <= g;
   consider R be Relation of S, S such that
A4:  for c, d be set holds [c,d] in R iff c in S & d in S & P[c,d]
      from Rel_On_Set_Ex;
A5:  for c, d be set holds [c,d] in R iff ex f,g be map of L,
      InclPoset Ids L st c = f & d = g &
     c in S & d in S & f <= g
    proof
     let c,d be set;
     hereby assume A6: [c,d] in R;
then A7:   c in S & d in S by A4;
     consider f,g be map of L,
       InclPoset Ids L such that A8: c = f & d = g & f <= g
        by A4,A6;
     thus ex f,g be map of L, InclPoset Ids L st
      c = f & d = g & c in S & d in S & f <= g by A7,A8;
     end;
     given f,g be map of L, InclPoset Ids L such that
A9:      c = f & d = g & c in S & d in S & f <= g;
     thus [c,d] in R by A4,A9;
    end;
   take RelStr (#S,R#);
   thus thesis by A2,A5;
  end;
  uniqueness
  proof
   let R1, R2 be strict RelStr;
   assume A10: ( a in the carrier of R1 iff
    ex s be map of L, InclPoset Ids L st a = s &
     s is monotone &
     for x be Element of L holds s.x c= downarrow x ) &
    for c, d be set holds [c,d] in the InternalRel of R1 iff
    ex f,g be map of L, InclPoset Ids L st
    c = f & d = g & c in the carrier of R1 & d in the carrier of R1 &
     f <= g;
   assume A11: ( a in the carrier of R2 iff
    ex s be map of L, InclPoset Ids L st a = s &
     s is monotone &
     for x be Element of L holds s.x c= downarrow x ) &
    for c, d be set holds [c,d] in the InternalRel of R2 iff
    ex f,g be map of L, InclPoset Ids L st
    c = f & d = g & c in the carrier of R2 & d in the carrier of R2 & f <= g;
A12: the carrier of R1 = the carrier of R2
   proof
     thus the carrier of R1 c= the carrier of R2
     proof
      let b be set; assume b in the carrier of R1;
      then consider s be map of L, InclPoset Ids L such that
A13:      b = s & s is monotone &
       for x be Element of L holds s.x c= downarrow x by A10;
      thus b in the carrier of R2 by A11,A13;
     end;
     thus the carrier of R2 c= the carrier of R1
     proof
      let b be set; assume b in the carrier of R2;
      then consider s be map of L, InclPoset Ids L such that
A14:      b = s & s is monotone &
       for x be Element of L holds s.x c= downarrow x by A11;
      thus b in the carrier of R1 by A10,A14;
     end;
   end;
     the InternalRel of R1 = the InternalRel of R2
   proof
     let c,d be set;
A15:   now assume [c,d] in the InternalRel of R1;
      then consider f,g be map of L, InclPoset Ids L such that
A16:    c = f & d = g & c in the carrier of R1 & d in the carrier of R1 &
        f <= g by A10;
      thus [c,d] in the InternalRel of R2 by A11,A12,A16;
     end;
       now assume [c,d] in the InternalRel of R2;
      then consider f,g be map of L, InclPoset Ids L such that
A17:    c = f & d = g & c in the carrier of R2 & d in the carrier of R2 &
         f <= g by A11;
      thus [c,d] in the InternalRel of R1 by A10,A12,A17;
     end; hence thesis by A15;
   end;
   hence thesis by A12;
  end;
end;

theorem
   for L being lower-bounded sup-Semilattice holds
  MonSet L is full SubRelStr of (InclPoset Ids L)|^(the carrier of L)
  proof
   let L be lower-bounded sup-Semilattice;
   set J = ((the carrier of L) --> InclPoset Ids L);
   A1: the carrier of MonSet L c=
        the carrier of (InclPoset Ids L)|^(the carrier of L)
   proof
    let a be set; assume a in the carrier of MonSet L;
    then consider s be map of L, InclPoset Ids L such that
A2:  a = s & s is monotone &
      for x be Element of L holds s.x c= downarrow x by Def14;
      s in Funcs (the carrier of L, the carrier of InclPoset Ids L)
      by FUNCT_2:11;
    hence thesis by A2,YELLOW_1:28;
   end;
A3:the InternalRel of MonSet L c=
       the InternalRel of (InclPoset Ids L)|^(the carrier of L)
   proof
    let a,b be set; assume [a,b] in the InternalRel of MonSet L;
    then consider f,g be map of L, InclPoset Ids L such that
A4:    a = f & b = g & a in the carrier of MonSet L &
       b in the carrier of MonSet L & f <= g by Def14;
    set AG = product ((the carrier of L) --> InclPoset Ids L);
A5:  AG = ((InclPoset Ids L) |^ the carrier of L) by YELLOW_1:def 5;
A6: f in Funcs (the carrier of L, the carrier of InclPoset Ids L) &
     g in Funcs (the carrier of L, the carrier of InclPoset Ids L)
       by FUNCT_2:11;
then A7: f in the carrier of AG & g in the carrier of AG by A5,YELLOW_1:28;
    reconsider f' = f, g' = g as Element of AG
       by A5,A6,YELLOW_1:28;
A8:  f' in product Carrier ((the carrier of L) --> InclPoset Ids L)
       by A7,YELLOW_1:def 4;
      ex ff,gg being Function st ff = f' & gg = g' &
     for i be set st i in the carrier of L
      ex R being RelStr, xi,yi being Element of R
       st R = J.i & xi = ff.i & yi = gg.i & xi <= yi
    proof
     take f,g;
     thus f = f' & g = g';
     let i be set; assume A9: i in the carrier of L;
     then reconsider i' = i as Element of L;
     take R = InclPoset Ids L;
     reconsider xi = f.i', yi = g.i' as Element of R;
     take xi, yi;
     thus R = J.i & xi = f.i & yi = g.i by A9,FUNCOP_1:13;
     reconsider i' = i as Element of L by A9;
     consider a, b be Element of InclPoset Ids L such that
A10:     a = f.i' & b = g.i' & a <= b by A4,YELLOW_2:def 1;
     thus thesis by A10;
    end;
    then f' <= g' by A8,YELLOW_1:def 4;
    then [a,b] in the InternalRel of
     product ((the carrier of L) --> InclPoset Ids L)
      by A4,ORDERS_1:def 9;
    hence thesis by YELLOW_1:def 5;
   end;
   set J = ((the carrier of L) --> InclPoset Ids L);
  the InternalRel of MonSet L =
    (the InternalRel of (InclPoset Ids L)|^(the carrier of L) )|_2
      the carrier of MonSet L
   proof
    let a,b be set;
    thus [a,b] in the InternalRel of MonSet L implies
   [a,b] in (the InternalRel of (InclPoset Ids L)|^(the carrier of L))|_2
      the carrier of MonSet L by A3,WELLORD1:16;
   assume [a,b] in (the InternalRel of (InclPoset Ids L)|^
     (the carrier of L) )|_2 the carrier of MonSet L;
then A11: [a,b] in (the InternalRel of (InclPoset Ids L)|^
     (the carrier of L) ) &
   [a,b] in [:the carrier of MonSet L, the carrier of MonSet L:]
     by WELLORD1:16;
then A12: a in the carrier of (InclPoset Ids L)|^(the carrier of L) &
      b in the carrier of (InclPoset Ids L)|^(the carrier of L)
       by ZFMISC_1:106;
then A13: a in the carrier of product J & b in the carrier of product J
     by YELLOW_1:def 5;
   reconsider a' = a, b' = b as Element of product J
     by A12,YELLOW_1:def 5;
     [a',b'] in (the InternalRel of product J) by A11,YELLOW_1:def 5;
then A14: a' <= b' by ORDERS_1:def 9;
     a' in product Carrier J by A13,YELLOW_1:def 4;
   then consider f,g being Function such that
A15:   f = a' & g = b' &
    for i be set st i in the carrier of L
     ex R being RelStr, xi,yi being Element of R
       st R = ((the carrier of L) --> InclPoset Ids L).i &
        xi = f.i & yi = g.i & xi <= yi by A14,YELLOW_1:def 4;
      f in Funcs (the carrier of L, the carrier of InclPoset Ids L) &
     g in Funcs (the carrier of L, the carrier of InclPoset Ids L)
      by A12,A15,YELLOW_1:28;
    then reconsider f, g as Function of the carrier of L,
      the carrier of InclPoset Ids L by FUNCT_2:121;
    reconsider f, g as map of L, InclPoset Ids L ;
      now take f, g;
       f <= g
     proof
      let j be set; assume j in the carrier of L;
      then reconsider j' = j as Element of L;
      take f.j', g.j';
      consider R being RelStr, xi,yi being Element of R such that
A16:     R = ((the carrier of L) --> InclPoset Ids L).j' &
        xi = f.j' & yi = g.j' & xi <= yi by A15;
      thus thesis by A16,FUNCOP_1:13;
     end;
     hence a' = f & b' = g & a' in the carrier of MonSet L &
      b' in the carrier of MonSet L & f <= g by A11,A15,ZFMISC_1:106;
    end;
    hence [a,b] in the InternalRel of MonSet L by Def14;
   end;
   hence MonSet L is full SubRelStr of
     (InclPoset Ids L)|^(the carrier of L) by A1,A3,YELLOW_0:def 13,def 14;
  end;

theorem Th17:
 for L being lower-bounded sup-Semilattice,
     AR being auxiliary(ii) Relation of L
  for x, y being Element of L holds
   x <= y implies AR-below x c= AR-below y
 proof
  let L be lower-bounded sup-Semilattice, AR be auxiliary(ii) Relation of L;
  let x, y be Element of L;
  assume A1: x <= y;
A2:AR-below x = {y1 where y1 is Element of L: [y1,x] in AR} by Def11;
  let a; assume a in AR-below x;
  then consider y2 be Element of L such that A3: y2 = a & [y2,x] in AR by A2;
    y2 <= y2;
  then [y2,y] in AR by A1,A3,Def5;
  hence thesis by A3,Th13;
 end;

definition let L be lower-bounded sup-Semilattice;
  let AR be auxiliary(ii) auxiliary(iii) auxiliary(iv) Relation of L;
  cluster AR-below -> monotone;
  coherence
  proof
   set s = AR-below;
   let x, y be Element of L;
A1: s.x = AR-below x & s.y = AR-below y by Def13;
   assume x <= y;
   then AR-below x c= AR-below y by Th17;
   hence thesis by A1,YELLOW_1:3;
  end;
end;

theorem Th18:
 for L being lower-bounded sup-Semilattice, AR being auxiliary Relation of L
  holds
   AR-below in the carrier of MonSet L
  proof
    let L be lower-bounded sup-Semilattice, AR be auxiliary Relation of L;
    set s = AR-below;
      ex s be map of L, InclPoset Ids L st
    AR-below = s & s is monotone &
     for x be Element of L holds s.x c= downarrow x
    proof
     take s;
       for x be Element of L holds s.x c= downarrow x
     proof
      let x be Element of L;
        s.x = AR-below x by Def13;
      hence s.x c= downarrow x by Th12;
     end;
     hence thesis;
    end;
    hence thesis by Def14;
  end;

definition let L be lower-bounded sup-Semilattice;
 cluster MonSet L -> non empty;
 coherence
 proof
  consider AR be auxiliary Relation of L;
    AR-below in the carrier of MonSet L by Th18;
  hence thesis by STRUCT_0:def 1;
 end;
end;

theorem Th19:
 for L being lower-bounded sup-Semilattice holds
  IdsMap L in the carrier of MonSet L
  proof
   let L be lower-bounded sup-Semilattice;
   set s = IdsMap L;
     ex s' be map of L, InclPoset Ids L st
   s = s' & s' is monotone & for x be Element of L holds s'.x c= downarrow x
   proof
    take s;
    thus thesis by YELLOW_2:def 4;
   end;
   hence thesis by Def14;
  end;

theorem
   for L being lower-bounded sup-Semilattice, AR being auxiliary Relation of L
  holds
   AR-below <= IdsMap L
  proof
   let L be lower-bounded sup-Semilattice, AR be auxiliary Relation of L;
   let x be set;
   assume x in the carrier of L;
   then reconsider x' = x as Element of L;
A1: (AR-below).x' = AR-below x' by Def13;
     (IdsMap L).x' = downarrow x' by YELLOW_2:def 4;
then A2: (AR-below).x c= (IdsMap L).x by A1,Th12;
   reconsider a = (AR-below).x',
       b = (IdsMap L).x' as Element of InclPoset Ids L;
   take a, b;
   thus thesis by A2,YELLOW_1:3;
  end;

theorem Th21:
 for L being lower-bounded non empty Poset
  for I being Ideal of L holds Bottom L in I
  proof
   let L be lower-bounded non empty Poset;
   let I be Ideal of L;
   consider x be Element of I;
     Bottom L <= x by YELLOW_0:44;
   hence thesis by WAYBEL_0:def 19;
  end;

theorem
   for L being upper-bounded non empty Poset
  for F being Filter of L holds Top L in F
  proof
   let L be upper-bounded non empty Poset;
   let F be Filter of L;
   consider x be Element of F;
     Top L >= x by YELLOW_0:45;
   hence thesis by WAYBEL_0:def 20;
  end;

theorem Th23:
 for L being lower-bounded non empty Poset holds
  downarrow Bottom L = {Bottom L}
 proof
   let L be lower-bounded non empty Poset;
   thus downarrow Bottom L c= {Bottom L}
  proof
    let a; assume a in downarrow Bottom L;
    then a in downarrow {Bottom L} by WAYBEL_0:def 17;
    then a in {x where x is Element of L : ex y being Element of L st x <= y &
      y in {Bottom L}} by WAYBEL_0:14;
    then consider a' be Element of L such that A1: a' = a &
       ex y being Element of L st a' <= y & y in {Bottom L};
    consider y being Element of L such that A2: a' <= y & y in {Bottom
L} by A1;
A3:  Bottom L <= a' by YELLOW_0:44;
      y = Bottom L by A2,TARSKI:def 1;
    hence thesis by A1,A2,A3,ORDERS_1:25;
   end;
    let a; assume a in {Bottom L};
then A4:  a = Bottom L by TARSKI:def 1;
      Bottom L <= Bottom L;
    hence thesis by A4,WAYBEL_0:17;
  end;

theorem
   for L being upper-bounded non empty Poset holds uparrow Top L = {Top L}
  proof let L be upper-bounded non empty Poset;
   thus uparrow Top L c= {Top L}
   proof
    let x be set; assume
A1:  x in uparrow Top L;
    then reconsider x as Element of L;
      x >= Top L & x <= Top L by A1,WAYBEL_0:18,YELLOW_0:45;
    then x = Top L by ORDERS_1:25;
    hence thesis by TARSKI:def 1;
   end;
   let x be set; assume x in {Top L};
   then x = Top L & Top L <= Top L by TARSKI:def 1;
   hence thesis by WAYBEL_0:18;
  end;

Lm5:
 for L being lower-bounded sup-Semilattice, I being Ideal of L holds
  {Bottom L} c= I
 proof
   let L be lower-bounded sup-Semilattice;
   let I be Ideal of L;
   let a; assume a in {Bottom L};
   then a = Bottom L by TARSKI:def 1;
   hence thesis by Th21;
  end;

reserve L for lower-bounded sup-Semilattice;
reserve x for Element of L;

theorem Th25:
 (the carrier of L) --> {Bottom L} is map of L, InclPoset Ids L
  proof
     {Bottom L} = downarrow Bottom L by Th23;
   then {Bottom L} in {X where X is Ideal of L: not contradiction};
   then {Bottom L} in Ids L by WAYBEL_0:def 23;
   then {Bottom L} in the carrier of InclPoset Ids L by YELLOW_1:1;
   then (the carrier of L) --> {Bottom L} is Function of the carrier of L,
      the carrier of InclPoset Ids L by FUNCOP_1:57;
   hence thesis ;
  end;

Lm6:
for f be map of L, InclPoset Ids L st f = (the carrier of L) --> {Bottom L}
  holds f is monotone
proof
 let f be map of L, InclPoset Ids L;
 assume A1: f = (the carrier of L) --> {Bottom L};
 let x,y be Element of L;
   f.x = {Bottom L} & f.y = {Bottom L} by A1,FUNCOP_1:13;
 hence thesis by YELLOW_1:3;
end;

theorem Th26:
 (the carrier of L) --> {Bottom L} in the carrier of MonSet L
proof
  set s = (the carrier of L) --> {Bottom L};
    ex s' be map of L, InclPoset Ids L st
  s = s' & s' is monotone &
   for x be Element of L holds s'.x c= downarrow x
  proof
   reconsider s as map of L, InclPoset Ids L by Th25;
   take s;
     for x holds s.x c= downarrow x
   proof
    let x be Element of L;
      s.x = {Bottom L} by FUNCOP_1:13;
    hence s.x c= downarrow x by Lm5;
   end;
   hence thesis by Lm6;
  end;
  hence thesis by Def14;
end;

theorem
   for AR being auxiliary Relation of L holds
  [(the carrier of L) --> {Bottom L} , AR-below] in the InternalRel of MonSet L
 proof
   let AR be auxiliary Relation of L;
   set c = (the carrier of L) --> {Bottom L}, d = AR-below;
     ex f,g be map of L, InclPoset Ids L st c = f & d = g &
     c in the carrier of MonSet L & d in the carrier of MonSet L & f <= g
   proof
    reconsider c as map of L, InclPoset Ids L by Th25;
    take c,d;
      c <= d
    proof
     let x be set; assume x in the carrier of L;
     then reconsider x' = x as Element of L;
       d.x = AR-below x' by Def13;
     then reconsider dx = d.x' as Ideal of L;
     reconsider dx' = dx as Element of InclPoset Ids L;
       c.x' = {Bottom L} by FUNCOP_1:13;
then A1:   c.x c= dx by Lm5;
     take c.x', dx';
     thus thesis by A1,YELLOW_1:3;
    end;
    hence thesis by Th18,Th26;
   end;
  hence thesis by Def14;
 end;

Lm7:
for L ex x be Element of MonSet L st x is_>=_than the carrier of MonSet L
proof
 let L;
 set x = IdsMap L;
   x in the carrier of MonSet L by Th19;
 then reconsider x as Element of MonSet L;
   x is_>=_than the carrier of MonSet L
 proof
  let b be Element of MonSet L;
  assume b in the carrier of MonSet L;
  consider s be map of L, InclPoset Ids L such that A1: b = s &
   s is monotone & for x be Element of L holds s.x c= downarrow x by Def14;
    IdsMap L >= s
  proof
   let a be set; assume a in the carrier of L;
   then reconsider a' = a as Element of L;
A2: (IdsMap L).a = downarrow a' by YELLOW_2:def 4;
A3: s.a c= downarrow a' by A1;
   reconsider A = s.a',
        B = (IdsMap L).a' as Element of InclPoset Ids L;
   take A, B;
   thus thesis by A2,A3,YELLOW_1:3;
  end;
  then [b,x] in the InternalRel of MonSet L by A1,Def14;
  hence thesis by ORDERS_1:def 9;
 end;
 hence thesis;
end;

definition let L;
  cluster MonSet L -> upper-bounded;
  coherence
  proof
   consider x be Element of MonSet L such that
A1:  x is_>=_than the carrier of MonSet L by Lm7;
   take x;
   thus thesis by A1;
  end;
end;

definition let L;
 func Rel2Map L -> map of InclPoset Aux L, MonSet L means :Def15:
  for AR being auxiliary Relation of L holds it.AR = AR-below;
 existence
 proof
 defpred P[set,set] means
  ex AR be auxiliary Relation of L st AR = $1 & $2 = AR-below;
A1: for a st a in the carrier of InclPoset Aux L
    ex y be set st y in the carrier of MonSet L & P[a,y]
   proof
    let a; assume a in the carrier of InclPoset Aux L;
    then a in Aux L by YELLOW_1:1;
    then reconsider AR = a as auxiliary Relation of L by Def9;
    take AR-below;
    thus thesis by Th18;
   end;
   consider f being Function of the carrier of InclPoset Aux L,
   the carrier of MonSet L such that
A2:  for a st a in the carrier of InclPoset Aux L holds P[a,f.a]
      from FuncEx1(A1);
   take f;
     now let AR be auxiliary Relation of L;
      AR in Aux L by Def9;
    then AR in the carrier of InclPoset Aux L by YELLOW_1:1;
    then P[AR,f.AR] by A2;
    hence f.AR = AR-below;
   end;
   hence thesis ;
 end;
 uniqueness
 proof
  let I1, I2 be map of InclPoset Aux L, MonSet L;
  assume A3: for AR be auxiliary Relation of L holds I1.AR = AR-below;
  assume A4: for AR be auxiliary Relation of L holds I2.AR = AR-below;
    dom I1 = the carrier of InclPoset Aux L by FUNCT_2:def 1;
then A5: dom I1 = Aux L by YELLOW_1:1;
    dom I2 = the carrier of InclPoset Aux L by FUNCT_2:def 1;
then A6: dom I2 = Aux L by YELLOW_1:1;
    now let a; assume a in Aux L;
   then reconsider AR = a as auxiliary Relation of L by Def9;
     I1.AR = AR-below by A3
        .= I2.AR by A4;
   hence I1.a = I2.a;
  end;
  hence thesis by A5,A6,FUNCT_1:9;
 end;
end;

theorem
   for R1, R2 being auxiliary Relation of L st R1 c= R2 holds
  R1-below <= R2-below
  proof
    let R1, R2 be auxiliary Relation of L; assume A1: R1 c= R2;
     let x be set;
     assume x in the carrier of L;
     then reconsider x' = x as Element of L;
A2:   R1-below x' c= R2-below x'
     proof
      let a; assume a in R1-below x';
      then a in {y where y is Element of L: [y,x'] in R1} by Def11;
      then consider b be Element of L such that A3: b = a & [b,x'] in R1;
        b in {y where y is Element of L: [y,x'] in R2} by A1,A3;
      hence thesis by A3,Def11;
     end;
    reconsider A1 = (R1-below).x', A2 = (R2-below).x'
       as Element of InclPoset Ids L;
    take A1, A2;
      (R1-below).x = R1-below x' &
        (R2-below).x = R2-below x' by Def13;
    hence thesis by A2,YELLOW_1:3;
  end;

theorem Th29:
  for R1, R2 being Relation of L st R1 c= R2 holds
   R1-below x c= R2-below x
   proof
    let R1, R2 be Relation of L; assume A1: R1 c= R2;
    let a; assume a in R1-below x;
    then a in {z where z is Element of L: [z,x] in R1} by Def11;
    then consider b be Element of L such that A2: b = a & [b,x] in R1;
      b in {z where z is Element of L: [z,x] in R2} by A1,A2;
    hence thesis by A2,Def11;
   end;

Lm8:
  Rel2Map L is monotone
 proof
   let x,y be Element of InclPoset Aux L;
     x in the carrier of InclPoset Aux L &
     y in the carrier of InclPoset Aux L;
   then x in Aux L & y in Aux L by YELLOW_1:1;
   then reconsider R1 = x, R2 = y as auxiliary Relation of L by Def9;
   assume x <= y;
then A1: x c= y by YELLOW_1:3;
   let a, b be Element of MonSet L;
   assume A2: a = (Rel2Map L).x & b = (Rel2Map L).y;
   thus a <= b
   proof
A3:  (Rel2Map L).x = R1-below & (Rel2Map L).y = R2-below by Def15;
    consider s be map of L, InclPoset Ids L such that
A4:  (Rel2Map L).x = s & s is monotone &
     for x be Element of L holds s.x c= downarrow x by Def14;
    consider t be map of L, InclPoset Ids L such that
A5:   (Rel2Map L).y = t & t is monotone &
     for x be Element of L holds t.x c= downarrow x by Def14;
      s <= t
    proof
     let q be set; assume q in the carrier of L;
     then reconsider q' = q as Element of L;
A6:    s.q = R1-below q' by A3,A4,Def13;
A7:    t.q = R2-below q' by A3,A5,Def13;
A8:     R1-below q' c= R2-below q' by A1,Th29;
       reconsider sq = s.q', tq = t.q' as Element of InclPoset Ids L;
         sq <= tq by A6,A7,A8,YELLOW_1:3;
     hence thesis;
    end;
    then [R1-below, R2-below] in the InternalRel of MonSet L
      by A3,A4,A5,Def14;
    hence thesis by A2,A3,ORDERS_1:def 9;
   end;
 end;

definition let L;
  cluster Rel2Map L -> monotone;
  coherence by Lm8;
end;

definition let L;
  func Map2Rel L -> map of MonSet L, InclPoset Aux L means :Def16:
   for s be set st s in the carrier of MonSet L
    ex AR be auxiliary Relation of L st AR = it.s &
      for x,y be set holds
       [x,y] in AR iff ex x',y' be Element of L,
        s' be map of L, InclPoset Ids L st
     x' = x & y' = y & s' = s & x' in s'.y';
   existence
   proof
    defpred P[set, set] means
      ex AR be auxiliary Relation of L st AR = $2 & for x,y be set holds
       [x,y] in AR iff ex x',y' be Element of L,
        s' be map of L, InclPoset Ids L st
         x' = x & y' = y & s' = $1 & x' in s'.y';
A1:  for a st a in the carrier of MonSet L ex b be set st b in the carrier of
         InclPoset Aux L & P[a,b]
   proof
    let a; assume A2: a in the carrier of MonSet L;
     defpred Q[set,set] means
       ex x', y' be Element of L, s' be map of L, InclPoset Ids L st
         x' = $1 & y' = $2 & s' = a & x' in s'.y';
     consider R being Relation of the carrier of L, the carrier of L such that
A3:    for x,y be set holds [x,y] in R iff
      x in the carrier of L & y in the carrier of L & Q[x,y]
       from Rel_On_Set_Ex;
     reconsider R as Relation of L ;
       now
      thus R is auxiliary(i)
      proof
       let x, y be Element of L;
       assume [x,y] in R;
       then consider x', y' be Element of L,
        s' be map of L, InclPoset Ids L such that
A4:       x' = x & y' = y & s' = a & x' in s'.y' by A3;
       consider s be map of L, InclPoset Ids L
        such that A5: a = s & s is monotone &
         for x be Element of L holds s.x c= downarrow x by A2,Def14;
         s'.y c= downarrow y by A4,A5;
       hence x <= y by A4,WAYBEL_0:17;
      end;
      thus R is auxiliary(ii)
      proof
       let x, y, z, u be Element of L;
       assume A6: u <= x & [x,y] in R & y <= z;
       then consider x', y' be Element of L,
        s' be map of L, InclPoset Ids L such that
A7:       x' = x & y' = y & s' = a & x' in s'.y' by A3;
       consider s be map of L, InclPoset Ids L
        such that A8: a = s & s is monotone &
         for x be Element of L holds s.x c= downarrow x by A2,Def14;
       reconsider sy = s.y, sz = s.z as Element of InclPoset Ids L;
         sy <= sz by A6,A8,ORDERS_3:def 5;
then A9:    s.y c= s.z by YELLOW_1:3;
         s.z in the carrier of InclPoset Ids L;
       then s.z in Ids L by YELLOW_1:1;
       then s.z in {X where X is Ideal of L: not contradiction} by WAYBEL_0:def
23;
       then consider sz be Ideal of L such that A10: s.z = sz;
         u in sz by A6,A7,A8,A9,A10,WAYBEL_0:def 19;
       hence thesis by A3,A8,A10;
      end;
      thus R is auxiliary(iii)
      proof
       let x, y, z be Element of L;
       assume A11: [x,z] in R & [y,z] in R;
       then consider x1, z1 be Element of L,
        s1 be map of L, InclPoset Ids L such that
A12:       x1 = x & z1 = z & s1 = a & x1 in s1.z1 by A3;
       consider y2, z2 be Element of L,
        s2 be map of L, InclPoset Ids L such that
A13:       y2 = y & z2 = z & s2 = a & y2 in s2.z2 by A3,A11;
         s1.z in the carrier of InclPoset Ids L;
       then s1.z in Ids L by YELLOW_1:1;
       then s1.z in {X where X is Ideal of L: not contradiction} by WAYBEL_0:
def 23;
       then consider sz be Ideal of L such that A14: s1.z = sz;
       consider z3 be Element of L such that A15: z3 in sz & x <= z3 & y <= z3
         by A12,A13,A14,WAYBEL_0:def 1;
          ex q being Element of L st x <= q & y <= q &
         for c being Element of L st x <= c & y <= c holds q <= c
           by LATTICE3:def 10;
       then x "\/" y <= z3 by A15,LATTICE3:def 13;
       then x "\/" y in sz by A15,WAYBEL_0:def 19;
       hence thesis by A3,A12,A14;
      end;
      thus R is auxiliary(iv)
      proof
       let x be Element of L;
       reconsider x' = Bottom L, y' = x as Element of L;
       consider s' be map of L, InclPoset Ids L
        such that A16: a = s' & s' is monotone &
         for x be Element of L holds s'.x c= downarrow x by A2,Def14;
         s'.y' in the carrier of InclPoset Ids L;
       then s'.y' in Ids L by YELLOW_1:1;
       then s'.y' in {X where X is Ideal of L: not contradiction}
          by WAYBEL_0:def 23;
       then consider sy be Ideal of L such that A17: sy = s'.y';
         x' in sy by Th21;
       hence thesis by A3,A16,A17;
      end;
     end;
     then reconsider R as auxiliary Relation of L by Def8;
A18: for x,y be set holds [x,y] in R iff
       ex x',y' be Element of L, s' be map of L, InclPoset Ids L st
        x' = x & y' = y & s' = a & x' in s'.y' by A3;
    take b = R;
      b in Aux L by Def9;
    hence thesis by A18,YELLOW_1:1;
   end;
  consider f being Function of the carrier of MonSet L, the carrier of
    InclPoset Aux L such that
A19: for a st a in
 the carrier of MonSet L holds P[a,f.a] from FuncEx1 (A1);
   reconsider f' = f as map of MonSet L, InclPoset Aux L
     ;
   take f';
   let s be set; assume A20: s in the carrier of MonSet L;
   then reconsider s' = s as Element of MonSet L;
     f'.s' in the carrier of InclPoset Aux L;
   then f'.s' in Aux L by YELLOW_1:1;
   then reconsider fs = f'.s' as auxiliary Relation of L by Def9;
   take fs;
     ex AR be auxiliary Relation of L st AR = f'.s & for x,y be set holds
    [x,y] in AR iff ex x',y' be Element of L,
      s' be map of L, InclPoset Ids L st
        x' = x & y' = y & s' = s & x' in s'.y' by A19,A20;
    hence thesis;
   end;
   uniqueness
   proof
    let M1, M2 be map of MonSet L, InclPoset Aux L;
    assume A21: for s be set st s in the carrier of MonSet L
     ex AR be auxiliary Relation of L st AR = M1.s &
      for x,y be set holds
       [x,y] in AR iff ex x',y' be Element of L,
       s' be map of L, InclPoset Ids L st
     x' = x & y' = y & s' = s & x' in s'.y';
    assume A22: for s be set st s in the carrier of MonSet L
     ex AR be auxiliary Relation of L st AR = M2.s &
      for x,y be set holds
       [x,y] in AR iff ex x',y' be Element of L,
       s' be map of L, InclPoset Ids L st
     x' = x & y' = y & s' = s & x' in s'.y';
      M1 = M2
    proof
A23:   dom M1 = the carrier of MonSet L by FUNCT_2:def 1;
A24:   dom M2 = the carrier of MonSet L by FUNCT_2:def 1;
       for s be set st s in the carrier of MonSet L holds M1.s = M2.s
     proof
      let s be set; assume A25: s in the carrier of MonSet L;
      then consider AR1 be auxiliary Relation of L such that A26: AR1 = M1.s &
      for x,y be set holds
       [x,y] in AR1 iff ex x',y' be Element of L,
       s' be map of L, InclPoset Ids L st
       x' = x & y' = y & s' = s & x' in s'.y' by A21;
      consider AR2 be auxiliary Relation of L such that A27: AR2 = M2.s &
      for x,y be set holds
       [x,y] in AR2 iff ex x',y' be Element of L,
       s' be map of L, InclPoset Ids L st
       x' = x & y' = y & s' = s & x' in s'.y' by A22,A25;
        AR1 = AR2
      proof
       let x,y be set;
       hereby assume [x,y] in AR1;
        then consider x',y' be Element of L,
         s' be map of L, InclPoset Ids L such that
A28:      x' = x & y' = y & s' = s & x' in s'.y' by A26;
        thus [x,y] in AR2 by A27,A28;
       end;
       assume [x,y] in AR2;
        then consider x',y' be Element of L,
         s' be map of L, InclPoset Ids L such that
A29:      x' = x & y' = y & s' = s & x' in s'.y' by A27;
       thus [x,y] in AR1 by A26,A29;
      end;
      hence thesis by A26,A27;
     end;
     hence thesis by A23,A24,FUNCT_1:9;
    end;
    hence thesis;
   end;
end;

Lm9:
 Map2Rel L is monotone
 proof
  set f = Map2Rel L;
A1:InclPoset Aux L = RelStr (#Aux L, RelIncl Aux L#) by YELLOW_1:def 1;
  let x,y be Element of MonSet L;
  assume x <= y;
  then [x,y] in the InternalRel of MonSet L by ORDERS_1:def 9;
  then consider s,t be map of L, InclPoset Ids L such that
A2:x = s & y = t & x in the carrier of MonSet L & y in
 the carrier of MonSet L &
   s <= t by Def14;
A3: f.s in the carrier of InclPoset Aux L &
    f.t in the carrier of InclPoset Aux L by A2,FUNCT_2:7;
then A4: f.s in Aux L & f.t in Aux L by YELLOW_1:1;
  then reconsider AS = f.s, AT = f.t as auxiliary Relation of L by Def9;
  reconsider AS' = AS, AT' = AT as Element of InclPoset Aux L
    by A3;
    AS' c= AT'
  proof
     for a,b be set st [a,b] in AS holds [a,b] in AT
   proof
    let a,b be set; assume A5: [a,b] in AS;
then A6:  a in the carrier of L & b in the carrier of L by ZFMISC_1:106;
    then reconsider a' = a, b' = b as Element of L;
    reconsider sb = s.b', tb = t.b' as Element of InclPoset Ids L;
    consider a1, b1 being Element of InclPoset Ids L such that
A7:    a1 = s.b & b1 = t.b & a1 <= b1 by A2,A6,YELLOW_2:def 1;
A8:  sb c= tb by A7,YELLOW_1:3;
    consider AR be auxiliary Relation of L such that A9: AR = f.x &
      for a',b' be set holds
       [a',b'] in AR iff ex x',y' be Element of L,
       s' be map of L, InclPoset Ids L st
     x' = a' & y' = b' & s' = x & x' in s'.y' by Def16;
    consider x',y' be Element of L,
       s' be map of L, InclPoset Ids L such that
A10:   x' = a' & y' = b' & s' = s & x' in s'.y' by A2,A5,A9;
    consider AR1 be auxiliary Relation of L such that A11: AR1 = f.y &
      for a',b' be set holds
       [a',b'] in AR1 iff ex x',y' be Element of L,
       s' be map of L, InclPoset Ids L st
     x' = a' & y' = b' & s' = y & x' in s'.y' by Def16;
    thus thesis by A2,A8,A10,A11;
   end;
   hence thesis by RELAT_1:def 3;
  end;
  then [AS',AT'] in RelIncl Aux L by A4,WELLORD2:def 1;
  hence thesis by A1,A2,ORDERS_1:def 9;
 end;

definition let L;
  cluster Map2Rel L -> monotone;
  coherence by Lm9;
end;

theorem Th30:
  (Map2Rel L) * (Rel2Map L) = id dom (Rel2Map L)
  proof
    set LS = (Map2Rel L) * (Rel2Map L);
    set R = id dom (Rel2Map L);
      dom LS = the carrier of InclPoset Aux L by FUNCT_2:def 1;
then A1:  dom LS = Aux L by YELLOW_1:1;
      dom R = dom (Rel2Map L) by FUNCT_1:34;
    then dom R = the carrier of InclPoset Aux L by FUNCT_2:def 1;
then A2:  dom R = Aux L by YELLOW_1:1;
      for a st a in Aux L holds LS.a = R.a
    proof
     let a; assume A3: a in Aux L;
     then reconsider AR = a as auxiliary Relation of L by Def9;
A4:  a in the carrier of InclPoset Aux L by A3,YELLOW_1:1;
then A5:   a in dom (Rel2Map L) by FUNCT_2:def 1;
     then LS.a = (Map2Rel L).((Rel2Map L).AR) by FUNCT_1:23;
then A6:   LS.a = (Map2Rel L).(AR-below) by Def15;
       LS.a in the carrier of InclPoset Aux L by A4,FUNCT_2:7;
     then LS.a in Aux L by YELLOW_1:1;
     then reconsider La = LS.a as auxiliary Relation of L by Def9;
A7:     AR-below in the carrier of MonSet L by Th18;
     La = AR
     proof
        for c,b be set holds [c,b] in La iff [c,b] in AR
      proof
       let c,b be set;
       hereby assume A8: [c,b] in La;
    consider AR' be auxiliary Relation of L such that A9:
      AR' = (Map2Rel L).(AR-below) &
      for c,b be set holds
       [c,b] in AR' iff ex c',b' be Element of L,
       s' be map of L, InclPoset Ids L st
     c' = c & b' = b & s' = AR-below & c' in s'.b' by A7,Def16;
     consider c',b' be Element of L,
       s' be map of L, InclPoset Ids L such that
A10:   c' = c & b' = b & s' = AR-below & c' in s'.b' by A6,A8,A9;
          c' in AR-below b' by A10,Def13;
        hence [c,b] in AR by A10,Th13;
       end;
       assume A11: [c,b] in AR;
       then c in the carrier of L & b in the carrier of L by ZFMISC_1:106;
       then reconsider c' = c, b' = b as Element of L;
         c' in AR-below b' by A11,Th13;
then A12:     c' in (AR-below).b' by Def13;
    consider AR' be auxiliary Relation of L such that
A13:   AR' = (Map2Rel L).(AR-below) &
      for c,b be set holds
       [c,b] in AR' iff ex c',b' be Element of L,
       s' be map of L, InclPoset Ids L st
     c' = c & b' = b & s' = AR-below & c' in s'.b' by A7,Def16;
       thus [c,b] in La by A6,A12,A13;
     end;
      hence thesis by RELAT_1:def 2;
     end;
     hence thesis by A5,FUNCT_1:35;
    end;
    hence LS = R by A1,A2,FUNCT_1:9;
  end;

theorem Th31:
  (Rel2Map L) * (Map2Rel L) = id (the carrier of MonSet L)
  proof
   set LS = (Rel2Map L) * (Map2Rel L);
   set R = id (the carrier of MonSet L);
A1: dom LS = the carrier of MonSet L by FUNCT_2:def 1;
A2: dom R = the carrier of MonSet L by FUNCT_1:34;
     for a st a in the carrier of MonSet L holds LS.a = R.a
   proof
    let a; assume A3: a in the carrier of MonSet L;
    then consider s be map of L, InclPoset Ids L such that
A4:   a = s & s is monotone &
     for x be Element of L holds s.x c= downarrow x by Def14;
      LS.s in the carrier of MonSet L by A3,A4,FUNCT_2:7;
    then consider Ls be map of L, InclPoset Ids L such that
A5:    LS.s = Ls & Ls is monotone &
     for x be Element of L holds Ls.x c= downarrow x by Def14;
    set AR = (Map2Rel L).s;
      AR in the carrier of InclPoset Aux L by A3,A4,FUNCT_2:7;
    then AR in Aux L by YELLOW_1:1;
    then reconsider AR as auxiliary Relation of L by Def9;
      dom (Map2Rel L) = the carrier of MonSet L by FUNCT_2:def 1;
    then Ls = (Rel2Map L).AR by A3,A4,A5,FUNCT_1:23;
then A6:  Ls = AR-below by Def15;
   Ls = s
    proof
A7:   dom Ls = the carrier of L by FUNCT_2:def 1;
A8:   dom s = the carrier of L by FUNCT_2:def 1;
       now let b be set; assume A9: b in the carrier of L;
      then reconsider b' = b as Element of L;
      thus Ls.b = s.b
      proof
       thus Ls.b c= s.b
       proof
        let d be set; assume d in Ls.b;
        then d in AR-below b' by A6,Def13;
then A10:      [d,b'] in AR by Th13;
    consider AR' be auxiliary Relation of L such that A11:
      AR' = (Map2Rel L).s & for d,b' be set holds
       [d,b'] in AR' iff ex d',b'' be Element of L,
       s' be map of L, InclPoset Ids L st
     d' = d & b'' = b' & s' = s & d' in s'.b'' by A3,A4,Def16;
       consider d',b'' be Element of L,
       s' be map of L, InclPoset Ids L such that
A12:   d' = d & b'' = b' & s' = s & d' in s'.b'' by A10,A11;
        thus thesis by A12;
       end;
       thus s.b c= Ls.b
       proof
        let d be set; assume A13: d in s.b;
          s.b in the carrier of InclPoset Ids L by A9,FUNCT_2:7;
        then s.b in Ids L by YELLOW_1:1;
        then s.b in {X where X is Ideal of L: not contradiction} by WAYBEL_0:
def 23;
        then consider X be Ideal of L such that A14: s.b = X;
        reconsider d' = d as Element of L by A13,A14;
    consider AR' be auxiliary Relation of L such that A15:
      AR' = (Map2Rel L).s & for d,b' be set holds
       [d,b'] in AR' iff ex d',b'' be Element of L,
       s' be map of L, InclPoset Ids L st
     d' = d & b'' = b' & s' = s & d' in s'.b'' by A3,A4,Def16;
          [d',b'] in AR by A13,A15;
        then d' in AR-below b' by Th13;
        hence thesis by A6,Def13;
       end;
      end;
     end;
     hence thesis by A7,A8,FUNCT_1:9;
    end;
    hence LS.a = R.a by A3,A4,A5,FUNCT_1:35;
   end;
   hence thesis by A1,A2,FUNCT_1:9;
  end;

definition let L;
  cluster Rel2Map L -> one-to-one;
  coherence
  proof
     ex g be Function st g*(Rel2Map L) = id dom (Rel2Map L)
   proof
    take Map2Rel L;
    thus thesis by Th30;
   end;
   hence Rel2Map L is one-to-one by FUNCT_1:53;
  end;
end;

:: Proposition 1.10 (i) p.43
theorem Th32:
  (Rel2Map L)" = Map2Rel L
  proof
      (Rel2Map L)*(Map2Rel L) = id (the carrier of MonSet L) implies
       rng (Rel2Map L) = the carrier of MonSet L by FUNCT_2:24;
   then Rel2Map L is one-to-one & rng (Rel2Map L) = dom (Map2Rel L) &
    (Map2Rel L)*(Rel2Map L) = id dom (Rel2Map L)
      by Th30,Th31,FUNCT_2:def 1;
   hence Map2Rel L = (Rel2Map L)" by FUNCT_1:63;
  end;

:: Proposition 1.10 (ii) p.43
theorem
    Rel2Map L is isomorphic
  proof
     ex g being map of MonSet L, InclPoset Aux L st
     g = (Rel2Map L)" & g is monotone
   proof
    reconsider g = Map2Rel L as map of MonSet L, InclPoset Aux L;
    take g;
    thus thesis by Th32;
   end;
   hence thesis by WAYBEL_0:def 38;
  end;

theorem Th34:
 for L being complete LATTICE, x being Element of L holds
  meet { I where I is Ideal of L : x <= sup I } = waybelow x
proof
  let L be complete LATTICE, x be Element of L;
  set X = { I where I is Ideal of L : x <= sup I };
    X c= bool the carrier of L
  proof
   let a; assume a in X;
   then consider I be Ideal of L such that A1: a = I & x <= sup I;
   thus thesis by A1;
  end;
  then reconsider X' = X as Subset-Family of L by SETFAM_1:def 7
;
    sup downarrow x = x by WAYBEL_0:34;
then A2:downarrow x in X;
 thus meet X c= waybelow x
 proof
  let a; assume A3: a in meet X;
  then a in meet X';
  then reconsider y = a as Element of L;
    now let I be Ideal of L; assume x <= sup I;
   then I in X;
   hence y in I by A3,SETFAM_1:def 1;
  end;
  then y << x by WAYBEL_3:21;
  hence thesis by WAYBEL_3:7;
 end;
 thus waybelow x c= meet X
 proof
  let a; assume a in waybelow x;
  then a in {y where y is Element of L: y << x} by WAYBEL_3:def 3;
  then consider a' be Element of L such that A4: a' = a & a' << x;
    for Y be set holds Y in X implies a in Y
  proof
   let Y be set; assume Y in X;
   then consider I be Ideal of L such that A5: Y = I & x <= sup I;
   thus thesis by A4,A5,WAYBEL_3:20;
  end;
  hence thesis by A2,SETFAM_1:def 1;
 end;
end;

scheme LambdaC'{ A() -> non empty RelStr, C[set], F(set) -> set,
  G(set) -> set } :
 ex f being Function st dom f = the carrier of A() &
  for x be Element of A() holds
   (C[x] implies f.x = F(x)) & (not C[x] implies f.x = G(x))
proof
  defpred c[set] means C[$1];
  deffunc f(set) = F($1);
  deffunc g(set) = G($1);
A1:  ex f being Function st dom f = the carrier of A() &
  for x be set st x in the carrier of A() holds
   (c[x] implies f.x = f(x)) & (not c[x] implies f.x = g(x)) from LambdaC;
 thus ex f being Function st dom f = the carrier of A() &
  for x be Element of A() holds
   (C[x] implies f.x = F(x)) & (not C[x] implies f.x = G(x))
     proof
      consider f being Function such that A2: dom f = the carrier of A() &
       for x be set st x in the carrier of A() holds
       (C[x] implies f.x = F(x)) & (not C[x] implies f.x = G(x)) by A1;
      take f;
      thus dom f = the carrier of A() by A2;
      let x be Element of A();
      thus (C[x] implies f.x = F(x)) & (not C[x] implies f.x = G(x)) by A2;
     end;
 end;

definition let L be Semilattice, I be Ideal of L;
  func DownMap I -> map of L, InclPoset Ids L means :Def17:
  for x be Element of L holds
   ( x <= sup I implies it.x = ( downarrow x ) /\ I ) &
   ( not x <= sup I implies it.x = downarrow x );
  existence
 proof
   defpred P[set,set] means
   for x be Element of L st x = $1 holds
    ( x <= sup I implies $2 = ( downarrow x ) /\ I ) &
    ( not x <= sup I implies $2 = downarrow x );
   defpred C[Element of L] means $1 <= sup I;
   deffunc F(Element of L) = ( downarrow $1 ) /\ I;
   deffunc G(Element of L) = downarrow $1;
 consider f being Function such that
A1: dom f = the carrier of L &
  for x be Element of L holds
    ( C[x] implies f.x = F(x) ) &
    ( not C[x] implies f.x = G(x) ) from LambdaC';
A2: for a be set st a in the carrier of L ex y be set st y in
     the carrier of InclPoset Ids L & P[a,y]
     proof let a; assume a in the carrier of L;
       then reconsider x = a as Element of L;
       take y = f.x;
       thus y in the carrier of InclPoset Ids L
      proof
        per cases;
        suppose x <= sup I;
        then y = ( downarrow x ) /\ I by A1;
        then y is Ideal of L by YELLOW_2:42;
        then y in {X where X is Ideal of L: not contradiction};
        then y in Ids L by WAYBEL_0:def 23;
        hence thesis by YELLOW_1:1;
        suppose not x <= sup I;
        then y = downarrow x by A1;
        then y in {X where X is Ideal of L: not contradiction};
        then y in Ids L by WAYBEL_0:def 23;
        hence thesis by YELLOW_1:1;
       end;
       thus P[a,y] by A1;
     end;
   consider f being Function of the carrier of L,
    the carrier of InclPoset Ids L such that
A3:   for a st a in the carrier of L holds P[a,f.a] from FuncEx1(A2);
   reconsider f as map of L, InclPoset Ids L ;
     for x be Element of L holds
    ( x <= sup I implies f.x = ( downarrow x ) /\ I ) &
    ( not x <= sup I implies f.x = downarrow x ) by A3;
   hence thesis;
  end;
  uniqueness
 proof
    let M1, M2 be map of L, InclPoset Ids L;
    assume A4: for x be Element of L holds
      ( x <= sup I implies M1.x = ( downarrow x ) /\ I ) &
       ( not x <= sup I implies M1.x = downarrow x );
    assume A5: for x be Element of L holds
      ( x <= sup I implies M2.x = ( downarrow x ) /\ I ) &
        ( not x <= sup I implies M2.x = downarrow x );
A6: dom M1 = the carrier of L by FUNCT_2:def 1;
A7: dom M2 = the carrier of L by FUNCT_2:def 1;
      now let x be set; assume x in the carrier of L;
     then reconsider x' = x as Element of L;
A8:  now assume A9: x' <= sup I;
      then M1.x' = ( downarrow x' ) /\ I by A4;
      hence M1.x' = M2.x' by A5,A9;
     end;
       now assume A10: not x' <= sup I;
      then M1.x' = downarrow x' by A4;
      hence M1.x' = M2.x' by A5,A10;
     end;
     hence M1.x = M2.x by A8;
    end;
    hence thesis by A6,A7,FUNCT_1:9;
  end;
end;

Lm10:
 for L be Semilattice, I be Ideal of L holds
  DownMap I is monotone
proof
  let L be Semilattice, I be Ideal of L;
  let x,y be Element of L;
  assume A1: x <= y;
  per cases;
  suppose x <= sup I & y <= sup I;
then A2: (DownMap I).x = (downarrow x) /\ I & (DownMap I).y = (downarrow y) /\
I by Def17;
    downarrow x c= downarrow y by A1,WAYBEL_0:21;
  then (DownMap I).x c= (DownMap I).y by A2,XBOOLE_1:26;
  hence thesis by YELLOW_1:3;
  suppose x <= sup I & not y <= sup I;
then A3: (DownMap I).x = (downarrow x) /\ I & (DownMap I).y = downarrow y by
Def17;
A4:downarrow x c= downarrow y by A1,WAYBEL_0:21;
    (downarrow x) /\ I c= downarrow x by XBOOLE_1:17;
  then (DownMap I).x c= (DownMap I).y by A3,A4,XBOOLE_1:1;
  hence thesis by YELLOW_1:3;
  suppose not x <= sup I & y <= sup I;
  hence thesis by A1,ORDERS_1:26;
  suppose not x <= sup I & not y <= sup I;
  then (DownMap I).x = downarrow x & (DownMap I).y = downarrow y by Def17;
  then (DownMap I).x c= (DownMap I).y by A1,WAYBEL_0:21;
  hence thesis by YELLOW_1:3;
 end;

Lm11:
for L be Semilattice, x be Element of L
 for I be Ideal of L holds (DownMap I).x c= downarrow x
proof
 let L be Semilattice, x be Element of L;
 let I be Ideal of L;
 per cases;
 suppose x <= sup I;
 then (DownMap I).x = (downarrow x) /\ I by Def17;
 hence thesis by XBOOLE_1:17;
 suppose not x <= sup I;
 hence thesis by Def17;
end;

theorem Th35:
 for L being Semilattice, I being Ideal of L holds
  DownMap I in the carrier of MonSet L
 proof
   let L be Semilattice, I be Ideal of L;
   reconsider mI = DownMap I as map of L, InclPoset Ids L;
     ex s be map of L, InclPoset Ids L st mI = s &
     s is monotone &
     for x be Element of L holds s.x c= downarrow x
  proof
    take mI;
    thus thesis by Lm10,Lm11;
   end;
   hence thesis by Def14;
  end;

theorem Th36:
 for L being with_infima antisymmetric reflexive RelStr, x being Element of L
 for D being non empty lower Subset of L holds
  {x} "/\" D = (downarrow x) /\ D
 proof
   let L be with_infima antisymmetric reflexive RelStr, x be Element of L;
   let D be non empty lower Subset of L;
A1: {x} "/\" D = { x' "/\" y where x', y is Element of L : x' in {x} & y in D }
      by YELLOW_4:def 4;
   thus {x} "/\" D c= (downarrow x) /\ D
  proof
    let a; assume a in {x} "/\" D;
    then a in { x' "/\" y where x', y is Element of L : x' in {x} & y in D }
     by YELLOW_4:def 4;
    then consider x', y be Element of L such that
A2:   a = x' "/\" y & x' in {x} & y in D;
    reconsider a' = a as Element of L by A2;
A3:  x' = x by A2,TARSKI:def 1;
      ex v being Element of L st x' >= v & y >= v &
      for c being Element of L st x' >= c & y >= c holds v >= c
       by LATTICE3:def 11;
then A4:  x' "/\" y <= x' & x' "/\" y <= y by LATTICE3:def 14;
then A5:  a in downarrow x by A2,A3,WAYBEL_0:17;
      a' in D by A2,A4,WAYBEL_0:def 19;
    hence a in (downarrow x) /\ D by A5,XBOOLE_0:def 3;
   end;
   thus (downarrow x) /\ D c= {x} "/\" D
  proof
    let a; assume A6: a in (downarrow x) /\ D;
then A7:  a in downarrow x & a in D by XBOOLE_0:def 3;
    reconsider a' = a as Element of D by A6,XBOOLE_0:def 3;
A8:  x in {x} by TARSKI:def 1;
      a' <= x by A7,WAYBEL_0:17;
    then a' = a' "/\" x by YELLOW_0:25;
    hence a in {x} "/\" D by A1,A8;
   end;
  end;

begin  :: Approximating Relations

:: Definition 1.11 p.44
definition let L be non empty RelStr, AR be Relation of L;
  attr AR is approximating means :Def18:
   for x be Element of L holds x = sup (AR-below x);
end;

definition let L be non empty Poset; let mp be map of L, InclPoset Ids L;
  attr mp is approximating means :Def19:
  for x be Element of L
   ex ii be Subset of L st ii = mp.x & x = sup ii;
end;

:: Lemma 1.12 (i) p.44
theorem Th37:
  for L being lower-bounded meet-continuous Semilattice, I being Ideal of L
    holds DownMap I is approximating
 proof
   let L be lower-bounded meet-continuous Semilattice;
   let I be Ideal of L;
     for x be Element of L ex ii be Subset of L st
      ii = (DownMap I).x & x = sup ii
  proof
    let x be Element of L;
    set ii = (DownMap I).x;
      ii in the carrier of InclPoset Ids L;
    then ii in Ids L by YELLOW_1:1;
    then ii in {X where X is Ideal of L: not contradiction} by WAYBEL_0:def 23
;
    then consider ii' be Ideal of L such that A1: ii' = ii;
    reconsider dI = ( downarrow x ) /\ I as Subset of L;
    per cases;
    suppose A2: x <= sup I;
    then sup ii' = sup dI by A1,Def17
           .= sup ({x} "/\" I) by Th36
           .= x "/\" sup I by WAYBEL_2:def 6
           .= x by A2,YELLOW_0:25;
    hence thesis by A1;
    suppose not x <= sup I;
    then sup ii' = sup downarrow x by A1,Def17
           .= x by WAYBEL_0:34;
    hence thesis by A1;
   end;
   hence thesis by Def19;
  end;

Lm12:
 for L be complete LATTICE, x be Element of L
  for D be directed Subset of L holds sup ({x} "/\" D) <= x
 proof
   let L be complete LATTICE, x be Element of L;
   let D be directed Subset of L;
A1: {x} "/\" D = { a "/\" b where a, b is Element of L : a in {x} & b in D }
      by YELLOW_4:def 4;
A2: ex_sup_of ({x} "/\" D),L by YELLOW_0:17;
     for c being Element of L st c in ({x} "/\" D) holds c <= x
  proof
    let c be Element of L; assume c in ({x} "/\" D);
    then consider a, b be Element of L such that
A3:    c = a "/\" b & a in {x} & b in D by A1;
      a = x by A3,TARSKI:def 1;
    hence c <= x by A3,YELLOW_0:23;
   end;
   then x is_>=_than ({x} "/\" D) by LATTICE3:def 9;
   hence sup ({x} "/\" D) <= x by A2,YELLOW_0:30;
  end;

:: Lemma 1.12 (ii) p.44
theorem Th38:
 for L being lower-bounded continuous LATTICE holds L is meet-continuous
proof
  let L be lower-bounded continuous LATTICE;
    now let D be non empty directed Subset of L;
   let x be Element of L; assume A1: x <= sup D;
A2:  ex_sup_of waybelow x,L & ex_sup_of downarrow (sup ({x} "/\" D)),L
      by YELLOW_0:17;
      waybelow x c= downarrow (sup ({x} "/\" D))
   proof
     let q be set; assume q in waybelow x;
     then q in {y where y is Element of L: y << x} by WAYBEL_3:def 3;
     then consider q' be Element of L such that A3: q' = q & q' << x;
A4:   q' <= x by A3,WAYBEL_3:1;
     consider d be Element of L such that
A5:            d in D & q' <= d by A1,A3,WAYBEL_3:def 1;
     x in {x} by TARSKI:def 1;
     then x "/\" d in { a "/\" b where a, b is Element of L : a in {x} & b in
 D } by A5;
     then A6: x "/\" d in {x} "/\" D by YELLOW_4:def 4;
       ex_inf_of {x,d},L by YELLOW_0:17;
then A7:   q' <= x "/\" d by A4,A5,YELLOW_0:19;
       sup ({x} "/\" D) is_>=_than {x} "/\" D by YELLOW_0:32;
     then x "/\" d <= sup ({x} "/\" D) by A6,LATTICE3:def 9;
     then q' <= sup ({x} "/\" D) by A7,ORDERS_1:26;
     hence thesis by A3,WAYBEL_0:17;
    end;
    then sup waybelow x <= sup downarrow (sup ({x} "/\" D)) by A2,YELLOW_0:34;
    then sup waybelow x <= sup ({x} "/\" D) by WAYBEL_0:34;
then A8:  x <= sup ({x} "/\" D) by WAYBEL_3:def 5;
      sup ({x} "/\" D) <= x by Lm12;
    hence x = sup ({x} "/\" D) by A8,ORDERS_1:25;
   end;
  then for x being Element of L, D being non empty directed Subset of L
   st x <= sup D holds x = sup ({x} "/\" D);
  hence thesis by WAYBEL_2:52;
 end;

definition
  cluster continuous -> meet-continuous (lower-bounded LATTICE);
  coherence by Th38;
end;

:: Lemma 1.12 (iii) p.44
theorem
   for L being lower-bounded continuous LATTICE,
     I being Ideal of L holds DownMap I is approximating by Th37;

definition let L be non empty reflexive antisymmetric RelStr;
  cluster L-waybelow -> auxiliary(i);
  coherence
 proof
   let x, y be Element of L;
   assume [x,y] in L-waybelow;
   then x << y by Def2;
   hence thesis by WAYBEL_3:1;
 end;
end;

definition let L be non empty reflexive transitive RelStr;
  cluster L-waybelow -> auxiliary(ii);
  coherence
 proof
   set AR = L-waybelow;
   let x, y, z, u be Element of L;
   assume u <= x & [x,y] in AR & y <= z;
   then u <= x & x << y & y <= z by Def2;
   then u << z by WAYBEL_3:2;
   hence [u,z] in AR by Def2;
  end;
end;

definition let L be with_suprema Poset;
  cluster L-waybelow -> auxiliary(iii);
  coherence
 proof
   set AR = L-waybelow;
   let x, y, z be Element of L;
   assume [x,z] in AR & [y,z] in AR;
   then x << z & y << z by Def2;
   then (x "\/" y) << z by WAYBEL_3:3;
   hence [(x "\/" y),z] in AR by Def2;
  end;
end;

definition let L be /\-complete (non empty Poset);
  cluster L-waybelow -> auxiliary(iii);
  coherence
 proof
   set AR = L-waybelow;
   let x, y, z be Element of L;
   assume [x,z] in AR & [y,z] in AR;
   then x << z & y << z by Def2;
   then (x "\/" y) << z by WAYBEL_3:3;
   hence [(x "\/" y),z] in AR by Def2;
  end;
end;

definition let L be lower-bounded antisymmetric reflexive non empty RelStr;
  cluster L-waybelow -> auxiliary(iv);
  coherence
 proof
   let x be Element of L;
     Bottom L << x by WAYBEL_3:4;
   hence thesis by Def2;
  end;
end;

theorem Th40:
 for L being complete LATTICE, x being Element of L holds
  (L-waybelow)-below x = waybelow x
 proof
    let L be complete LATTICE, x be Element of L;
    set AR = L-waybelow;
A1:  AR-below x = {y where y is Element of L: [y,x] in AR} by Def11;
    set A = {y where y is Element of L: [y,x] in AR};
    set B = {y where y is Element of L: y << x};
      A = B
    proof
     thus A c= B
     proof
       let a be set;
       assume a in A;
       then consider v being Element of L such that
A2:    a = v and
A3:    [v,x] in AR;
         v << x by A3,Def2;
       hence a in { u' where u' is Element of L : u' << x } by A2;
      end;
      thus B c= A
     proof
        let a be set;
        assume a in B;
        then consider v being Element of L such that
A4:     a = v and
A5:     v << x;
          [v,x] in AR by A5,Def2;
        hence a in { u' where u' is Element of L : [u',x] in AR } by A4;
      end;
    end;
    hence thesis by A1,WAYBEL_3:def 3;
  end;

theorem Th41:
 for L being LATTICE holds IntRel L is approximating
 proof
    let L be LATTICE;
    set AR = IntRel L;
    let x be Element of L;
    set A = {y where y is Element of L: [y,x] in AR};
    set E = { u where u is Element of L : u <= x };
A1:  {y where y is Element of L: [y,x] in AR} = E
   proof
      thus A c= E
     proof
       let a be set; assume a in A;
       then consider v being Element of L such that
A2:    a = v and
A3:    [v,x] in AR;
         v <= x by A3,Lm1;
       hence a in E by A2;
      end;
      thus E c= A
     proof
       let a be set; assume a in E;
       then consider v being Element of L such that
A4:    a = v and
A5:    v <= x;
         [v,x] in AR by A5,Lm1;
       hence a in A by A4;
      end;
    end;
      {y where y is Element of L: y <= x } c= the carrier of L
   proof let z be set; assume z in {y where y is Element of L: y <= x };
      then ex y being Element of L st z = y & y <= x;
      hence thesis;
    end;
    then reconsider E as Subset of L;
A6:  x is_>=_than E
   proof
     let b be Element of L; assume b in E;
     then consider b' be Element of L such that A7: b' = b & b' <= x;
     thus b <= x by A7;
    end;
      now
      let b be Element of L; assume A8: b is_>=_than E;
        x in E;
      hence x <= b by A8,LATTICE3:def 9;
    end;
    then sup E = x by A6,YELLOW_0:30;
    hence thesis by A1,Def11;
  end;

Lm13:
 for L be lower-bounded continuous LATTICE holds
  L-waybelow is approximating
proof
  let L be lower-bounded continuous LATTICE;
  let x be Element of L;
    x = sup waybelow x by WAYBEL_3:def 5;
  hence thesis by Th40;
end;

definition let L be lower-bounded continuous LATTICE;
  cluster L-waybelow -> approximating;
  coherence by Lm13;
end;

definition let L be complete LATTICE;
  cluster approximating auxiliary Relation of L;
  existence
proof
  reconsider A = IntRel L as auxiliary Relation of L;
    A is approximating by Th41;
  hence thesis;
end;
end;

definition let L be complete LATTICE;
    defpred P[set] means
        $1 is approximating auxiliary Relation of L;
  func App L means :Def20:
   a in it iff a is approximating auxiliary Relation of L;
   existence
  proof
     consider X be set such that
A1:    for a holds a in X iff a in Aux L & P[a] from Separation;
     take X;
       a is approximating auxiliary Relation of L implies a in X
    proof
       assume A2: a is approximating auxiliary Relation of L;
       then a in Aux L by Def9;
       hence thesis by A1,A2;
     end;
     hence thesis by A1;
   end;
   uniqueness
    proof
      thus for X1,X2 being set st
      (for x being set holds x in X1 iff P[x]) &
      (for x being set holds x in X2 iff P[x]) holds X1 = X2 from SetEq;
    end;
end;

definition let L be complete LATTICE;
  cluster App L -> non empty;
  coherence
 proof
  consider a be approximating auxiliary Relation of L;
    a in App L by Def20;
  hence thesis;
 end;
end;

theorem Th42:
 for L being complete LATTICE
  for mp being map of L, InclPoset Ids L st
   mp is approximating & mp in the carrier of MonSet L
    ex AR being approximating auxiliary Relation of L st AR = (Map2Rel L).mp
proof
  let L be complete LATTICE;
  let mp be map of L, InclPoset Ids L;
  assume A1: mp is approximating & mp in the carrier of MonSet L;
  then consider AR be auxiliary Relation of L such that A2: AR = (Map2Rel L).mp
&
    for x,y be set holds [x,y] in AR iff ex x',y' be Element of L,
       s' be map of L, InclPoset Ids L st
     x' = x & y' = y & s' = mp & x' in s'.y' by Def16;
    now let x be Element of L;
   consider ii be Subset of L such that A3: ii = mp.x & x = sup ii by A1,Def19;
     AR-below x = mp.x
  proof
    thus AR-below x c= mp.x
   proof
     let a; assume a in AR-below x;
     then [a,x] in AR by Th13;
     then consider x',y' be Element of L,
       s' be map of L, InclPoset Ids L such that
A4:   x' = a & y' = x & s' = mp & x' in s'.y' by A2;
     thus thesis by A4;
    end;
    thus mp.x c= AR-below x
   proof
     let a; assume A5: a in mp.x;
     then reconsider a' = a as Element of L by A3;
       [a',x] in AR by A2,A5;
     hence thesis by Th13;
    end;
   end;
   hence x = sup (AR-below x) by A3;
  end;
  then reconsider AR as approximating auxiliary Relation of L by Def18;
  take AR;
  thus thesis by A2;
 end;

theorem Th43:
 for L being complete LATTICE, x being Element of L holds
  meet { (DownMap I).x where I is Ideal of L : not contradiction} = waybelow x
 proof
   let L be complete LATTICE, x be Element of L;
   set A = { (DownMap I).x where I is Ideal of L : not contradiction};
   set A1 = { (DownMap I).x where I is Ideal of L : x <= sup I};
A1: A1 = { (downarrow x) /\ I where I is Ideal of L : x <= sup I}
  proof
    thus A1 c= { (downarrow x) /\ I where I is Ideal of L : x <= sup I}
   proof
     let a; assume a in A1;
     then consider I1 be Ideal of L such that A2: a = (DownMap I1).x & x <= sup
I1;
       a = (downarrow x) /\ I1 by A2,Def17;
     hence a in { (downarrow x) /\ I where I is Ideal of L : x <= sup I} by A2
;
    end;
    thus { (downarrow x) /\ I where I is Ideal of L : x <= sup I} c= A1
   proof
     let a;
     assume a in { (downarrow x) /\ I where I is Ideal of L : x <= sup I};
     then consider I1 be Ideal of L such that
A3:     a = (downarrow x) /\ I1 & x <= sup I1;
       a = (DownMap I1).x by A3,Def17;
     hence a in A1 by A3;
    end;
   end;
   set A2 = { (DownMap I).x where I is Ideal of L : not x <= sup I};
A4: A2 = { downarrow x where I is Ideal of L : not x <= sup I}
  proof
    thus A2 c= { downarrow x where I is Ideal of L : not x <= sup I}
   proof
     let a; assume a in A2;
     then consider I1 be Ideal of L such that A5: a = (DownMap I1).x &
       not x <= sup I1;
       a = (downarrow x) by A5,Def17;
     hence a in { (downarrow x) where I is Ideal of L : not x <= sup I} by A5;
    end;
    thus { (downarrow x) where I is Ideal of L : not x <= sup I} c= A2
   proof
     let a;
     assume a in { (downarrow x) where I is Ideal of L : not x <= sup I};
     then consider I1 be Ideal of L such that
A6:     a = (downarrow x) & not x <= sup I1;
       a = (DownMap I1).x by A6,Def17;
     hence a in A2 by A6;
    end;
   end;
A7: A = A1 \/ A2
  proof
    thus A c= A1 \/ A2
   proof
     let a; assume a in A;
     then consider I2 be Ideal of L such that A8: a = (DownMap I2).x;
       x <= sup I2 or not x <= sup I2;
     then a in A1 or a in A2 by A8;
     hence thesis by XBOOLE_0:def 2;
    end;
    thus A1 \/ A2 c= A
   proof
     let a; assume a in A1 \/ A2;
     then a in A1 or a in A2 by XBOOLE_0:def 2;
     then consider I2,I3 be Ideal of L such that
A9:     ( a = (DownMap I2).x & x <= sup I2)
       or ( a = (DownMap I3).x & not x <= sup I3);
     per cases by A9;
     suppose ( a = (DownMap I2).x & x <= sup I2 );
     hence thesis;
     suppose ( a = (DownMap I3).x & not x <= sup I3);
     hence thesis;
    end;
   end;
   per cases;
   suppose A10: x = Bottom L;
A11:   A2 = {}
  proof
    assume A2 <> {};
    then reconsider A2' = A2 as non empty set;
    consider a be Element of A2';
      a in A2';
     then consider I1 be Ideal of L such that
A12:     a = downarrow x & not x <= sup I1 by A4;
    thus contradiction by A10,A12,YELLOW_0:44;
   end;
   set Dx = downarrow x;
     x <= sup Dx by A10,YELLOW_0:44;
then A13: Dx /\ Dx in A1 by A1;
      A1 c= { K where K is Ideal of L : x <= sup K}
   proof
     let a; assume a in A1;
     then consider H be Ideal of L such that
A14:     a = (downarrow x) /\ H & x <= sup H by A1;
     reconsider a' = a as Ideal of L by A14,YELLOW_2:42;
       x <= sup a' by A10,YELLOW_0:44;
     hence thesis;
    end;
then A15: meet { K where K is Ideal of L : x <= sup K} c= meet A1 by A13,
SETFAM_1:7;
A16: meet A1 = {x}
  proof
    reconsider I' = downarrow x as Ideal of L;
      x <= sup I' by A10,YELLOW_0:44;
    then (downarrow x) /\ I' in A1 by A1;
    then {x} in A1 by A10,Th23;
    hence meet A1 c= {x} by SETFAM_1:4;
      for Z1 be set st Z1 in A1 holds {x} c= Z1
   proof
     let Z1 be set; assume Z1 in A1;
     then consider Z1' be Ideal of L such that
A17:     Z1 = (downarrow x) /\ Z1' & x <= sup Z1' by A1;
A18:   {x} c= Z1' by A10,Lm5;
       {x} c= downarrow x by A10,Th23;
     hence thesis by A17,A18,XBOOLE_1:19;
    end;
    hence {x} c= meet A1 by A13,SETFAM_1:6;
   end;
   consider E be Ideal of L;
     x <= sup E by A10,YELLOW_0:44;
then A19: E in { K where K is Ideal of L : x <= sup K};
     for Z1 be set st Z1 in { K where K is Ideal of L : x <= sup K}
        holds meet A1 c= Z1
  proof
    let Z1 be set; assume Z1 in { K where K is Ideal of L : x <= sup K};
    then consider K1 be Ideal of L such that A20: K1 = Z1 & x <= sup K1;
    thus thesis by A10,A16,A20,Lm5;
   end;
   then meet A1 c= meet { K where K is Ideal of L : x <= sup K} by A19,SETFAM_1
:6;
   then meet A1 = meet { K where K is Ideal of L : x <= sup K} by A15,XBOOLE_0:
def 10;
   hence thesis by A7,A11,Th34;
   suppose A21: Bottom L <> x;
    set O = downarrow Bottom L;
A22:  sup O = Bottom L by WAYBEL_0:34;
    then sup O <= x by YELLOW_0:44;
    then not x < sup O by ORDERS_1:30;
    then not x <= sup O by A21,A22,ORDERS_1:def 10;
then A23: downarrow x in A2 by A4;
   reconsider O1 = downarrow x as Ideal of L;
A24: x <= sup O1 by WAYBEL_0:34;
      downarrow x = downarrow x /\ O1;
then A25:  downarrow x in A1 & downarrow x in { downarrow x where I is Ideal of
L :
        x <= sup I } by A1,A24;
A26: meet A2 = downarrow x
  proof
    thus meet A2 c= downarrow x by A23,SETFAM_1:4;
      now let Z1 be set; assume Z1 in A2;
     then consider L1 be Ideal of L such that A27: Z1 = downarrow x &
       not x <= sup L1 by A4;
     thus downarrow x c= Z1 by A27;
    end;
    hence downarrow x c= meet A2 by A23,SETFAM_1:6;
   end;
A28: meet A = (meet A1) /\ (meet A2) by A7,A23,A25,SETFAM_1:10;
A29: meet A1 c= downarrow x by A25,SETFAM_1:4;
then A30: meet A = meet A1 by A26,A28,XBOOLE_1:28;
A31: meet A1 c= (downarrow x) /\
      meet { I where I is Ideal of L : x <= sup I}
  proof
    let a; assume A32: a in meet A1;
    thus a in (downarrow x) /\
      meet { I where I is Ideal of L : x <= sup I}
   proof
     reconsider L' = [#]L as Subset of L;
       x in the carrier of L;
then A33:  x in L' by PRE_TOPC:12;
       ex_sup_of L',L by YELLOW_0:17;
     then L' is_<=_than sup L' by YELLOW_0:def 9;
     then x <= sup L' by A33,LATTICE3:def 9;
then A34:   L' in { I where I is Ideal of L : x <= sup I};
       a in meet { I where I is Ideal of L : x <= sup I}
    proof
         now let Y1 be set;
       assume Y1 in { I where I is Ideal of L : x <= sup I};
       then consider Y1' be Ideal of L such that
A35:       Y1 = Y1' & x <= sup Y1';
A36:    (downarrow x) /\ Y1' c= Y1' by XBOOLE_1:17;
         (downarrow x) /\ Y1' in A1 by A1,A35;
       then a in (downarrow x) /\ Y1' by A32,SETFAM_1:def 1;
       hence a in Y1 by A35,A36;
      end;
      hence thesis by A34,SETFAM_1:def 1;
     end;
     hence thesis by A29,A32,XBOOLE_0:def 3;
    end;
   end;
     (downarrow x) /\ meet { I where I is Ideal of L : x <= sup I} c= meet A1
  proof
    let a; assume a in (downarrow x) /\
      meet { I where I is Ideal of L : x <= sup I};
then A37:  a in downarrow x &
     a in meet { I where I is Ideal of L : x <= sup I} by XBOOLE_0:def 3;
    thus a in meet A1
   proof
      now let Y1 be set; assume Y1 in { (downarrow x) /\ I
          where I is Ideal of L : x <= sup I};
    then consider I1 be Ideal of L such that
A38:   Y1 = (downarrow x) /\ I1 & x <= sup I1;
        I1 in { I where I is Ideal of L : x <= sup I} by A38;
      then a in I1 by A37,SETFAM_1:def 1;
      hence a in Y1 by A37,A38,XBOOLE_0:def 3;
     end;
     hence thesis by A1,A25,SETFAM_1:def 1;
    end;
   end;
   then (downarrow x) /\ meet { I where I is Ideal of L : x <= sup I} = meet
A1
      by A31,XBOOLE_0:def 10;
then A39: (downarrow x) /\ waybelow x = meet A1 by Th34;
     waybelow x c= downarrow x by WAYBEL_3:11;
   hence thesis by A30,A39,XBOOLE_1:28;
  end;

:: Proposition 1.13 p.45
theorem Th44:
for L being lower-bounded meet-continuous LATTICE, x being Element of L holds
  meet {AR-below x where AR is auxiliary Relation of L : AR in App L}
    = waybelow x
proof
  let L be lower-bounded meet-continuous LATTICE, x be Element of L;
  set A = {AR-below x where AR is auxiliary Relation of L
    : AR in App L};
  consider AA be approximating auxiliary Relation of L;
    AA in App L by Def20;
then A1:AA-below x in A;
A2: meet { I where I is Ideal of L : x <= sup I } = waybelow x by Th34;
A3: meet { (DownMap I).x where I is Ideal of L : not contradiction } =
     waybelow x by Th43;
   consider I1 be Ideal of L;
A4: (DownMap I1).x in { (DownMap I).x where I is Ideal of L :
     not contradiction };
    { (DownMap I).x where I is Ideal of L : not contradiction } c= A
 proof
   let a be set;
   assume a in { (DownMap I).x where I is Ideal of L : not contradiction };
   then consider I be Ideal of L such that A5: a = (DownMap I).x;
A6: DownMap I is approximating by Th37;
A7: DownMap I in the carrier of MonSet L by Th35;
   then consider AR be auxiliary Relation of L such that
A8: AR = (Map2Rel L).(DownMap I) &
    for x,y be set holds [x,y] in AR iff ex x',y' be Element of L,
       s' be map of L, InclPoset Ids L st
     x' = x & y' = y & s' = DownMap I & x' in s'.y' by Def16;
   consider AR1 be approximating auxiliary Relation of L such that
A9:    AR1 = (Map2Rel L).(DownMap I) by A6,A7,Th42;
   consider ii be Subset of L such that
A10: ii = (DownMap I).x & x = sup ii by A6,Def19;
A11: AR-below x = (DownMap I).x
  proof
    thus AR-below x c= (DownMap I).x
   proof
     let a; assume a in AR-below x;
     then [a,x] in AR by Th13;
     then consider x',y' be Element of L,
       s' be map of L, InclPoset Ids L such that
A12:   x' = a & y' = x & s' = DownMap I & x' in s'.y' by A8;
     thus thesis by A12;
    end;
    thus (DownMap I).x c= AR-below x
   proof
     let a; assume A13: a in (DownMap I).x;
     then reconsider a' = a as Element of L by A10;
       [a',x] in AR by A8,A13;
     hence thesis by Th13;
    end;
   end;
     AR in App L by A8,A9,Def20;
   hence a in A by A5,A11;
  end;
  hence meet A c= waybelow x by A3,A4,SETFAM_1:7;
  thus waybelow x c= meet A
 proof
     A c= { I where I is Ideal of L : x <= sup I }
  proof
    let a; assume a in A;
    then consider AR be auxiliary Relation of L such that
A14:     a = AR-below x & AR in App L;
    reconsider AR as approximating auxiliary Relation of L by A14,Def20;
      sup (AR-below x) = x by Def18;
    hence a in { I where I is Ideal of L : x <= sup I } by A14;
   end;
   hence thesis by A1,A2,SETFAM_1:7;
  end;
 end;

reserve L for complete LATTICE;

:: Proposition 1.14 p.45   ( 1 <=> 2 )
theorem Th45:
   L is continuous iff
    (for R being approximating auxiliary Relation of L holds
      L-waybelow c= R & L-waybelow is approximating)
proof
  set AR = L-waybelow;
  hereby assume A1: L is continuous;
   then reconsider L' = L as lower-bounded meet-continuous LATTICE by Th38;
   thus for R be approximating auxiliary Relation of L holds AR c= R
      & AR is approximating
  proof
    let R be approximating auxiliary Relation of L;
    reconsider R' = R as approximating auxiliary Relation of L';
      for a,b be set st [a,b] in AR holds [a,b] in R
   proof
     let a,b be set; assume A2: [a,b] in AR;
     then a in the carrier of L & b in the carrier of L by ZFMISC_1:106;
     then reconsider a' = a, b' = b as Element of L';
       a' << b' by A2,Def2;
then A3:   a' in waybelow b' by WAYBEL_3:7;
A4:   meet { A1-below b' where A1 is auxiliary Relation of L' :
       A1 in App L' } = waybelow b' by Th44;
       R' in App L' by Def20;
     then R'-below b' in
     { A1-below b' where A1 is auxiliary Relation of L' :
        A1 in App L' };
     then waybelow b' c= R'-below b' by A4,SETFAM_1:4;
     hence thesis by A3,Th13;
    end;
    hence AR c= R by RELAT_1:def 3;
    thus AR is approximating by A1,Lm13;
   end;
  end;
  assume A5: for R be approximating auxiliary Relation of L holds AR c= R
         & AR is approximating;
    for x being Element of L holds x = sup waybelow x
 proof
   let x be Element of L;
   x = sup (AR-below x) by A5,Def18;
   hence x = sup waybelow x by Th40;
  end;
then A6:L is satisfying_axiom_of_approximation by WAYBEL_3:def 5;
    for x being Element of L holds waybelow x is non empty directed;
  hence L is continuous by A6,WAYBEL_3:def 6;
 end;

:: Proposition 1.14 p.45   ( 1 <=> 3 )
theorem
    L is continuous iff
   (L is meet-continuous &
    ex R being approximating auxiliary Relation of L st
     for R' being approximating auxiliary Relation of L holds R c= R')
 proof
   hereby assume A1: L is continuous;
    hence L is meet-continuous by Th38;
    reconsider R = L-waybelow as approximating auxiliary Relation of L
      by A1,Lm13;
    take R;
    thus for R' be approximating auxiliary Relation of L holds R c= R'
      by A1,Th45;
   end;
   assume A2: L is meet-continuous;
   given R be approximating auxiliary Relation of L such that
A3:   for R' be approximating auxiliary Relation of L holds R c= R';
     for x being Element of L holds x = sup waybelow x
  proof
    let x be Element of L;
    set K = {AR-below x where AR is auxiliary Relation of L :
      AR in App L};
A4:  meet K = waybelow x by A2,Th44;
      R in App L by Def20;
then A5:  R-below x in K;
then A6:  waybelow x c= R-below x by A4,SETFAM_1:4;
A7:  sup (R-below x) = x by Def18;
   for a st a in K holds R-below x c= a
   proof
     let a; assume a in K;
     then consider AA be auxiliary Relation of L such that
A8:      a = AA-below x & AA in App L;
     reconsider AA as approximating auxiliary Relation of L by A8,Def20;
     let b be set; assume A9: b in R-below x;
       R c= AA by A3;
     then R-below x c= AA-below x by Th29;
     hence thesis by A8,A9;
    end;
    then R-below x c= meet K by A5,SETFAM_1:6;
    hence thesis by A4,A6,A7,XBOOLE_0:def 10;
   end;
then A10: L is satisfying_axiom_of_approximation by WAYBEL_3:def 5;
     for x being Element of L holds waybelow x is non empty directed;
   hence L is continuous by A10,WAYBEL_3:def 6;
  end;

:: Definition 1.15 (SI) p.46
definition let L be RelStr, AR be Relation of L;
  attr AR is satisfying_SI means :Def21:
   for x, z be Element of L holds
   ( [x,z] in AR & x <> z implies
     ex y be Element of L st ( [x,y] in AR & [y,z] in AR & x <> y ) );
  synonym AR satisfies_SI;
end;

:: Definition 1.15 (INT) p.46
definition let L be RelStr, AR be Relation of L;
  attr AR is satisfying_INT means :Def22:
   for x, z be Element of L holds
   ( [x,z] in AR implies
    ex y be Element of L st ( [x,y] in AR & [y,z] in AR ) );
  synonym AR satisfies_INT;
end;

canceled;

theorem Th48:
for L being RelStr, AR being Relation of L
 holds AR satisfies_SI implies AR satisfies_INT
proof
   let L be RelStr, AR be Relation of L;
   assume A1: AR satisfies_SI;
   let x, z be Element of L;
      [x,z] in AR implies ex y be Element of L st ( [x,y] in AR & [y,z] in AR )
  proof
     assume A2: [x,z] in AR;
     per cases;
     suppose x <> z;
     then consider y be Element of L such that
A3:     ( [x,y] in AR & [y,z] in AR & x <> y ) by A1,A2,Def21;
     thus ex y be Element of L st ( [x,y] in AR & [y,z] in AR ) by A3;
     suppose x = z;
     hence ex y be Element of L st ( [x,y] in AR & [y,z] in AR ) by A2;
   end;
   hence thesis;
 end;

definition let L be non empty RelStr;
  cluster satisfying_SI -> satisfying_INT Relation of L;
  coherence by Th48;
end;

reserve AR for Relation of L;
reserve x, y, z for Element of L;

theorem Th49:
 for AR being approximating Relation of L st
  not x <= y holds ex u being Element of L st [u,x] in AR & not u <= y
 proof
    let AR be approximating Relation of L;
    assume
A1:  not x <= y;
      x = sup (AR-below x) & ex_sup_of (AR-below x),L
          by Def18,YELLOW_0:17;
     then y is_>=_than (AR-below x) implies y >= x by YELLOW_0:def 9;
    then consider u being Element of L such that
A2:   u in AR-below x & not u <= y by A1,LATTICE3:def 9;
    take u; thus [u,x] in AR & not u <= y by A2,Th13;
  end;

:: Lemma 1.16 p.46
theorem Th50:
 for R being approximating auxiliary(i) auxiliary(iii) Relation of L holds
  ( [x,z] in R & x <> z ) implies
   ex y st x <= y & [y,z] in R & x <> y
proof
   let R be approximating auxiliary(i) auxiliary(iii) Relation of L;
   assume A1: [x,z] in R & x <> z;
   then x <= z by Def4;
   then x < z by A1,ORDERS_1:def 10;
   then not z < x by ORDERS_1:28;
   then not z <= x by A1,ORDERS_1:def 10;
   then consider u be Element of L such that
A2:  [u,z] in R & not u <= x by Th49;
   take y = x "\/" u;
   thus x <= y by YELLOW_0:22;
   thus [y,z] in R by A1,A2,Def6;
   thus x <> y by A2,YELLOW_0:24;
 end;

:: Lemma 1.17 p.46
theorem Th51:
 for R being approximating auxiliary Relation of L holds
  ( x << z & x <> z ) implies
   ex y being Element of L st [x,y] in R & [y,z] in R & x <> y
proof
  let R be approximating auxiliary Relation of L;
  assume A1: x << z & x <> z;
  set I = {u where u is Element of L : ex y be Element of L st
           [u,y] in R & [y,z] in R };
A2:[Bottom L,Bottom L] in R by Def7;
    [Bottom L,z] in R by Def7;
then A3:Bottom L in I by A2;
    I c= the carrier of L
 proof let v be set; assume v in I;
   then ex u1 being Element of L st v = u1 & ex y be Element of L st
           [u1,y] in R & [y,z] in R;
   hence thesis;
  end;
  then reconsider I as non empty Subset of L by A3;
A4:I is lower
 proof
    let x1,y1 be Element of L;
    assume A5: x1 in I & y1 <= x1;
    then consider v1 be Element of L such that A6: v1 = x1 &
      ex s1 be Element of L st [v1,s1] in R & [s1,z] in R;
    consider s1 be Element of L such that A7: [v1,s1] in R & [s1,z] in R by A6;
      s1 <= s1;
    then [y1, s1] in R by A5,A6,A7,Def5;
    hence thesis by A7;
  end;
    I is directed
  proof
    let u1,u2 be Element of L; assume A8: u1 in I & u2 in I;
    then consider v1 be Element of L such that A9: v1 = u1 &
      ex y1 be Element of L st [v1,y1] in R & [y1,z] in R;
    consider v2 be Element of L such that A10: v2 = u2 &
      ex y2 be Element of L st [v2,y2] in R & [y2,z] in R by A8;
    consider y1 be Element of L such that A11: [v1,y1] in R & [y1,z] in
 R by A9;
    consider y2 be Element of L such that A12: [v2,y2] in R & [y2,z] in
 R by A10;
    take u1 "\/" u2;
A13: [u1 "\/" u2 , y1 "\/" y2] in R by A9,A10,A11,A12,Th1;
      [y1 "\/" y2 , z] in R by A11,A12,Def6;
    hence thesis by A13,YELLOW_0:22;
  end;
  then reconsider I as Ideal of L by A4;
    sup I = z
  proof
   set z' = sup I;
   assume A14: z' <> z;
A15:I c= R-below z
   proof
     let a be set; assume a in I;
     then consider u be Element of L such that
A16:    a = u & ex y2 be Element of L st [u,y2] in R & [y2,z] in R;
     consider y2 be Element of L such that A17: [u,y2] in R & [y2,z] in
 R by A16;
A18:   u <= y2 by A17,Def4;
       z <= z;
     then [u,z] in R by A17,A18,Def5;
     then a in {y where y is Element of L: [y,z] in R} by A16;
     hence thesis by Def11;
   end;
     ex_sup_of I,L & ex_sup_of (R-below z),L by YELLOW_0:17;
then A19:sup I <= sup (R-below z) by A15,YELLOW_0:34;
     z = sup (R-below z) by Def18;
   then z' < z by A14,A19,ORDERS_1:def 10;
   then not z <= z' by ORDERS_1:30;
   then consider y be Element of L such that
A20:  [y, z] in R & not y <= z' by Th49;
   consider u be Element of L such that
A21:  [u, y] in R & not u <= z' by A20,Th49;
A22:u in I by A20,A21;
     z' = "\/"(I,L) & ex_sup_of I,L iff z' is_>=_than I &
   for b being Element of L st b is_>=_than I holds z' <= b by YELLOW_0:30;
   hence contradiction by A21,A22,LATTICE3:def 9,YELLOW_0:17;
  end;
  then x in I by A1,WAYBEL_3:20;
  then consider v be Element of L such that
A23: v = x & ex y' be Element of L st [v,y'] in R & [y',z] in R;
  consider y' be Element of L such that A24: [v,y'] in R & [y',z] in R by A23;
A25: x <= y' by A23,A24,Def4;
    z <= z;
  then [x,z] in R by A24,A25,Def5;
  then consider y'' be Element of L such that
A26: x <= y'' & [y'',z] in R & x <> y'' by A1,Th50;
A27: x < y'' by A26,ORDERS_1:def 10;
  set Y = y' "\/" y'';
A28: y' <= Y & y'' <= Y by YELLOW_0:22;
then A29: x <> Y by A27,ORDERS_1:32;
     x <= x;
then A30: [x,Y] in R by A23,A24,A28,Def5;
    [Y,z] in R by A24,A26,Def6;
  hence thesis by A29,A30;
 end;

:: Theorem 1.18 p.47
theorem Th52:
 for L being lower-bounded continuous LATTICE holds
  L-waybelow satisfies_SI
 proof
    let L be lower-bounded continuous LATTICE;
    set R = L-waybelow;
    thus R satisfies_SI
   proof
     let x,z be Element of L;
     assume A1: [x,z] in R & x <> z;
     then x << z by Def2;
     hence thesis by A1,Th51;
    end;
  end;

definition let L be lower-bounded continuous LATTICE;
  cluster L-waybelow -> satisfying_SI;
  coherence by Th52;
end;

theorem Th53:
 for L being lower-bounded continuous LATTICE,
     x,y being Element of L st x << y
   ex x' being Element of L st x << x' & x' << y
  proof
     let L be lower-bounded continuous LATTICE;
     let x,y be Element of L;
     set R = L-waybelow;
     assume x << y;
  then [x,y] in R by Def2;
     then consider x' be Element of L such that A1: [x,x'] in R & [x',y] in R
       by Def22;
       x << x' & x' << y by A1,Def2;
     hence thesis;
   end;

:: Corollary 1.19 p.47
theorem
   for L being lower-bounded continuous LATTICE holds
   for x,y being Element of L holds
   ( x << y iff
    for D being non empty directed Subset of L st y <= sup D
        ex d being Element of L st d in D & x << d )
proof
  let L be lower-bounded continuous LATTICE;
  let x,y be Element of L;
  hereby assume A1: x << y;
   let D be non empty directed Subset of L;
   assume A2: y <= sup D;
   consider x' be Element of L such that A3: x << x' & x' << y by A1,Th53;
   consider d be Element of L such that
A4:  d in D & x' <= d by A2,A3,WAYBEL_3:def 1;
     x << d by A3,A4,WAYBEL_3:2;
   hence ex d be Element of L st d in D & x << d by A4;
  end;
  assume A5: for D be non empty directed Subset of L st y <= sup D
    ex d be Element of L st d in D & x << d;
    for D being non empty directed Subset of L st y <= sup D
   ex d being Element of L st d in D & x <= d
 proof
    let D be non empty directed Subset of L;
    assume y <= sup D;
    then consider d be Element of L such that A6: d in D & x << d by A5;
      x <= d by A6,WAYBEL_3:1;
    hence thesis by A6;
  end;
  hence thesis by WAYBEL_3:def 1;
 end;

begin :: Exercises

definition
 let L be RelStr, X be Subset of L,
     R be Relation of the carrier of L;
 pred X is_directed_wrt R means :Def23:
  for x,y being Element of L st x in X & y in X
   ex z being Element of L st z in X & [x,z] in R & [y,z] in R;
end;

theorem
    for L being RelStr, X being Subset of L st
   X is_directed_wrt (the InternalRel of L) holds X is directed
 proof
  let L be RelStr, X be Subset of L;
  assume A1: X is_directed_wrt (the InternalRel of L);
  let x,y be Element of L; assume x in X & y in X;
  then consider z being Element of L such that
A2:  z in X & [x,z] in the InternalRel of L & [y,z] in the InternalRel of L
    by A1,Def23;
  take z;
  thus z in X by A2;
  thus x <= z & y <= z by A2,ORDERS_1:def 9;
 end;

definition
 let X, x be set;
 let R be Relation;
  pred x is_maximal_wrt X,R means :Def24:
   x in X & not ex y being set st y in X & y <> x & [x,y] in R;
end;

definition
 let L be RelStr, X be set, x be Element of L;
  pred x is_maximal_in X means :Def25:
   x is_maximal_wrt X, the InternalRel of L;
end;

theorem
   for L being RelStr, X being set, x being Element of L holds
  x is_maximal_in X iff
    x in X & not ex y being Element of L st y in X & x < y
 proof
  let L be RelStr, X be set, x be Element of L;
  hereby assume x is_maximal_in X;
then A1:x is_maximal_wrt X, the InternalRel of L by Def25;
   hence x in X by Def24;
   let y be Element of L;
   per cases by A1,Def24;
   suppose not y in X;
   hence not y in X or not x < y;
   suppose y = x;
   hence not y in X or not x < y;
   suppose not [x,y] in the InternalRel of L;
   then not x <= y by ORDERS_1:def 9;
   hence not y in X or not x < y by ORDERS_1:def 10;
  end;
  assume A2: x in X & not ex y be Element of L st y in X & x < y;
  assume not x is_maximal_in X;
  then not x is_maximal_wrt X, the InternalRel of L by Def25;
  then consider y be set such that
A3: y in X & y <> x & [x,y] in the InternalRel of L by A2,Def24;
    y in the carrier of L by A3,ZFMISC_1:106;
  then reconsider y as Element of L;
    x <= y by A3,ORDERS_1:def 9;
  then x < y by A3,ORDERS_1:def 10;
  hence thesis by A2,A3;
 end;

definition
 let X, x be set;
 let R be Relation;
  pred x is_minimal_wrt X,R means :Def26:
   x in X & not ex y being set st y in X & y <> x & [y,x] in R;
end;

definition
 let L be RelStr, X be set, x be Element of L;
  pred x is_minimal_in X means :Def27:
   x is_minimal_wrt X, the InternalRel of L;
end;

theorem
   for L being RelStr, X being set, x being Element of L holds
  x is_minimal_in X iff
    x in X & not ex y being Element of L st y in X & x > y
 proof
  let L be RelStr, X be set, x be Element of L;
  hereby assume x is_minimal_in X;
then A1: x is_minimal_wrt X, the InternalRel of L by Def27;
   hence x in X by Def26;
   let y be Element of L;
   per cases by A1,Def26;
   suppose not y in X;
   hence not y in X or not x > y;
   suppose y = x;
   hence not y in X or not x > y;
   suppose not [y,x] in the InternalRel of L;
   then not y <= x by ORDERS_1:def 9;
   hence not y in X or not y < x by ORDERS_1:def 10;
  end;
  assume A2: x in X & not ex y be Element of L st y in X & x > y;
  assume not x is_minimal_in X;
  then not x is_minimal_wrt X, the InternalRel of L by Def27;
  then consider y be set such that
A3: y in X & y <> x & [y,x] in the InternalRel of L by A2,Def26;
    y in the carrier of L by A3,ZFMISC_1:106;
  then reconsider y as Element of L;
    y <= x by A3,ORDERS_1:def 9;
  then y < x by A3,ORDERS_1:def 10;
  hence thesis by A2,A3;
 end;

:: Exercise 1.23 (i)    ( 1 => 2 )
theorem
   AR satisfies_SI implies
  ( for x holds ( ex y st y is_maximal_wrt (AR-below x), AR )
    implies [x,x] in AR )
proof
 assume A1: AR satisfies_SI;
 let x;
 given y such that A2: y is_maximal_wrt (AR-below x), AR;
A3:  y in AR-below x & not ex y' be Element of L st
     y' in AR-below x & y <> y' & [y,y'] in AR by A2,Def24;
 assume A4: not [x,x] in AR;
A5: [y,x] in AR by A3,Th13;
 per cases;
 suppose x = y;
 hence contradiction by A3,A4,Th13;
 suppose x <> y;
 then consider z such that A6: [y,z] in AR & [z,x] in AR & z <> y by A1,A5,
Def21;
   z in AR-below x by A6,Th13;
 hence contradiction by A2,A6,Def24;
end;

:: Exercise 1.23 (i)    ( 2 => 1 )
theorem
   ( for x holds ( ex y st y is_maximal_wrt (AR-below x), AR )
   implies [x,x] in AR ) implies AR satisfies_SI
proof
 assume A1: for x holds ( ex y st y is_maximal_wrt (AR-below x), AR )
    implies [x,x] in AR;
   now let z,x; assume A2: [z,x] in AR & z <> x;
then A3: z in AR-below x by Th13;
  per cases;
  suppose [x,x] in AR;
  hence ex y st ( [z,y] in AR & [y,x] in AR & z <> y ) by A2;
  suppose not [x,x] in AR;
  then not z is_maximal_wrt (AR-below x), AR by A1;
  then consider y being set such that
A4:  y in AR-below x & y <> z & [z,y] in AR by A3,Def24;
  [y,x] in AR by A4,Th13;
  hence ex y st [z,y] in AR & [y,x] in AR & z <> y by A4;
 end;
 hence thesis by Def21;
end;

:: Exercise 1.23 (ii)    ( 3 => 4 )
theorem
   for AR being auxiliary(ii) auxiliary(iii) Relation of L holds
  AR satisfies_INT implies
   ( for x holds AR-below x is_directed_wrt AR)
proof
 let AR be auxiliary(ii) auxiliary(iii) Relation of L;
 assume A1: AR satisfies_INT;
 let x,y,z;
 assume y in AR-below x & z in AR-below x;
then A2: [y,x] in AR & [z,x] in AR by Th13;
 then consider y' be Element of L such that
A3: [y,y'] in AR & [y',x] in AR by A1,Def22;
 consider z' be Element of L such that
A4: [z,z'] in AR & [z',x] in AR by A1,A2,Def22;
 take u = y' "\/" z';
   [u,x] in AR by A3,A4,Def6;
 hence u in AR-below x by Th13;
   y <= y & y' <= u by YELLOW_0:22;
 hence [y,u] in AR by A3,Def5;
   z <= z & z' <= u by YELLOW_0:22;
 hence [z,u] in AR by A4,Def5;
end;

:: Exercise 1.23 (ii)    ( 4 => 3 )
theorem
   ( for x holds AR-below x is_directed_wrt AR) implies AR satisfies_INT
proof
 assume A1: for x holds AR-below x is_directed_wrt AR;
 let X,Z be Element of L;
 assume [X,Z] in AR;
then A2: X in AR-below Z by Th13;
   AR-below Z is_directed_wrt AR by A1;
 then consider u be Element of L such that
A3: u in AR-below Z & [X,u] in AR & [X,u] in AR by A2,Def23;
 take u;
 thus [X,u] in AR by A3;
 thus [u,Z] in AR by A3,Th13;
end;

:: Exercise 1.23 (iii) p.51
theorem Th62:
 for R being approximating auxiliary(i) auxiliary(ii) auxiliary(iii)
   Relation of L st
  R satisfies_INT holds R satisfies_SI
 proof
   let R be approximating auxiliary(i) auxiliary(ii) auxiliary(iii)
    Relation of L;
   assume A1: R satisfies_INT;
   let x, z;
   assume A2: [x,z] in R & x <> z;
   then consider y such that A3: ( [x,y] in R & [y,z] in R ) by A1,Def22;
   consider y' be Element of L such that A4: x <= y' & [y',z] in R & x <> y'
     by A2,Th50;
A5: x < y' by A4,ORDERS_1:def 10;
   take Y = y "\/" y';
A6: x <= y by A3,Def4;
A7: x <= x & y <= Y by YELLOW_0:22;
   per cases;
   suppose y' <= y;
   then x < y by A5,ORDERS_1:32;
   hence thesis by A3,A4,A7,Def5,Def6,ORDERS_1:32;
   suppose not y' <= y;
   then y <> Y by YELLOW_0:24;
   then y < Y by A7,ORDERS_1:def 10;
   hence thesis by A3,A4,A6,A7,Def5,Def6,ORDERS_1:32;
  end;

definition let L;
  cluster satisfying_INT ->
    satisfying_SI (approximating auxiliary Relation of L);
  coherence by Th62;
end;


Back to top