yellow_2.miz

    begin

    reserve x,X,Y for set;

    theorem :: YELLOW_2:1

    for L be non empty RelStr holds for x be Element of L holds for X be Subset of L holds X c= ( downarrow x) iff X is_<=_than x by WAYBEL_0: 17;

    theorem :: YELLOW_2:2

    for L be non empty RelStr holds for x be Element of L holds for X be Subset of L holds X c= ( uparrow x) iff x is_<=_than X by WAYBEL_0: 18;

    theorem :: YELLOW_2:3

    for L be antisymmetric transitive with_suprema RelStr holds for X,Y be set st ex_sup_of (X,L) & ex_sup_of (Y,L) holds ex_sup_of ((X \/ Y),L) & ( "\/" ((X \/ Y),L)) = (( "\/" (X,L)) "\/" ( "\/" (Y,L)))

    proof

      let L be antisymmetric transitive with_suprema RelStr;

      let X,Y be set such that

       A1: ex_sup_of (X,L) and

       A2: ex_sup_of (Y,L);

      set a = (( "\/" (X,L)) "\/" ( "\/" (Y,L)));



       A3: (X \/ Y) is_<=_than a

      proof

        let x be Element of L;

        assume

         A4: x in (X \/ Y);

        per cases by A4, XBOOLE_0:def 3;

          suppose

           A5: x in X;

          X is_<=_than ( "\/" (X,L)) by A1, YELLOW_0: 30;

          then

           A6: x <= ( "\/" (X,L)) by A5;

          ( "\/" (X,L)) <= a by YELLOW_0: 22;

          hence thesis by A6, ORDERS_2: 3;

        end;

          suppose

           A7: x in Y;

          Y is_<=_than ( "\/" (Y,L)) by A2, YELLOW_0: 30;

          then

           A8: x <= ( "\/" (Y,L)) by A7;

          ( "\/" (Y,L)) <= a by YELLOW_0: 22;

          hence thesis by A8, ORDERS_2: 3;

        end;

      end;

      for b be Element of L st (X \/ Y) is_<=_than b holds a <= b

      proof

        let b be Element of L;

        assume

         A9: (X \/ Y) is_<=_than b;

        Y c= (X \/ Y) by XBOOLE_1: 7;

        then Y is_<=_than b by A9;

        then

         A10: ( "\/" (Y,L)) <= b by A2, YELLOW_0: 30;

        X c= (X \/ Y) by XBOOLE_1: 7;

        then X is_<=_than b by A9;

        then ( "\/" (X,L)) <= b by A1, YELLOW_0: 30;

        hence thesis by A10, YELLOW_0: 22;

      end;

      hence thesis by A3, YELLOW_0: 30;

    end;

    theorem :: YELLOW_2:4

    for L be antisymmetric transitive with_infima RelStr holds for X,Y be set st ex_inf_of (X,L) & ex_inf_of (Y,L) holds ex_inf_of ((X \/ Y),L) & ( "/\" ((X \/ Y),L)) = (( "/\" (X,L)) "/\" ( "/\" (Y,L)))

    proof

      let L be antisymmetric transitive with_infima RelStr;

      let X,Y be set such that

       A1: ex_inf_of (X,L) and

       A2: ex_inf_of (Y,L);

      set a = (( "/\" (X,L)) "/\" ( "/\" (Y,L)));



       A3: (X \/ Y) is_>=_than a

      proof

        let x be Element of L;

        assume

         A4: x in (X \/ Y);

        per cases by A4, XBOOLE_0:def 3;

          suppose

           A5: x in X;

          X is_>=_than ( "/\" (X,L)) by A1, YELLOW_0: 31;

          then

           A6: x >= ( "/\" (X,L)) by A5;

          ( "/\" (X,L)) >= a by YELLOW_0: 23;

          hence thesis by A6, ORDERS_2: 3;

        end;

          suppose

           A7: x in Y;

          Y is_>=_than ( "/\" (Y,L)) by A2, YELLOW_0: 31;

          then

           A8: x >= ( "/\" (Y,L)) by A7;

          ( "/\" (Y,L)) >= a by YELLOW_0: 23;

          hence thesis by A8, ORDERS_2: 3;

        end;

      end;

      for b be Element of L st (X \/ Y) is_>=_than b holds a >= b

      proof

        let b be Element of L;

        assume

         A9: (X \/ Y) is_>=_than b;

        Y c= (X \/ Y) by XBOOLE_1: 7;

        then Y is_>=_than b by A9;

        then

         A10: ( "/\" (Y,L)) >= b by A2, YELLOW_0: 31;

        X c= (X \/ Y) by XBOOLE_1: 7;

        then X is_>=_than b by A9;

        then ( "/\" (X,L)) >= b by A1, YELLOW_0: 31;

        hence thesis by A10, YELLOW_0: 23;

      end;

      hence thesis by A3, YELLOW_0: 31;

    end;

    begin

    theorem :: YELLOW_2:5



     Th5: for R be Relation holds for X,Y be set holds X c= Y implies (R |_2 X) c= (R |_2 Y)

    proof

      let R be Relation, X,Y be set;

      assume

       A1: X c= Y;

      then (X |` R) c= (Y |` R) by RELAT_1: 100;

      then

       A2: ((X |` R) | X) c= ((Y |` R) | X) by RELAT_1: 76;

      ((Y |` R) | X) c= ((Y |` R) | Y) by A1, RELAT_1: 75;

      then ((X |` R) | X) c= ((Y |` R) | Y) by A2;

      then (R |_2 X) c= ((Y |` R) | Y) by WELLORD1: 10;

      hence thesis by WELLORD1: 10;

    end;

    theorem :: YELLOW_2:6

    for L be RelStr holds for S,T be full SubRelStr of L st the carrier of S c= the carrier of T holds the InternalRel of S c= the InternalRel of T

    proof

      let L be RelStr, S1,S2 be full SubRelStr of L;

      the InternalRel of S1 = (the InternalRel of L |_2 the carrier of S1) & the InternalRel of S2 = (the InternalRel of L |_2 the carrier of S2) by YELLOW_0:def 14;

      hence thesis by Th5;

    end;

    theorem :: YELLOW_2:7



     Th7: for L be non empty RelStr holds for S be non empty SubRelStr of L holds (X is directed Subset of S implies X is directed Subset of L) & (X is filtered Subset of S implies X is filtered Subset of L)

    proof

      let L be non empty RelStr;

      let S be non empty SubRelStr of L;

      thus X is directed Subset of S implies X is directed Subset of L

      proof

        assume

         A1: X is directed Subset of S;

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

        then

        reconsider X as Subset of L by A1, XBOOLE_1: 1;

        for x,y be Element of L st x in X & y in X holds ex z be Element of L st z in X & x <= z & y <= z

        proof

          let x,y be Element of L;

          assume

           A2: x in X & y in X;

          then

          reconsider x9 = x, y9 = y as Element of S by A1;

          consider z be Element of S such that

           A3: z in X & x9 <= z & y9 <= z by A1, A2, WAYBEL_0:def 1;

          reconsider z as Element of L by YELLOW_0: 58;

          take z;

          thus thesis by A3, YELLOW_0: 59;

        end;

        hence thesis by WAYBEL_0:def 1;

      end;

      thus X is filtered Subset of S implies X is filtered Subset of L

      proof

        assume

         A4: X is filtered Subset of S;

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

        then

        reconsider X as Subset of L by A4, XBOOLE_1: 1;

        for x,y be Element of L st x in X & y in X holds ex z be Element of L st z in X & z <= x & z <= y

        proof

          let x,y be Element of L;

          assume

           A5: x in X & y in X;

          then

          reconsider x9 = x, y9 = y as Element of S by A4;

          consider z be Element of S such that

           A6: z in X & z <= x9 & z <= y9 by A4, A5, WAYBEL_0:def 2;

          reconsider z as Element of L by YELLOW_0: 58;

          take z;

          thus thesis by A6, YELLOW_0: 59;

        end;

        hence thesis by WAYBEL_0:def 2;

      end;

    end;

    theorem :: YELLOW_2:8

    for L be non empty RelStr holds for S,T be non empty full SubRelStr of L st the carrier of S c= the carrier of T holds for X be Subset of S holds X is Subset of T & for Y be Subset of T st X = Y holds (X is filtered implies Y is filtered) & (X is directed implies Y is directed)

    proof

      let L be non empty RelStr, S1,S2 be non empty full SubRelStr of L;

      assume

       A1: the carrier of S1 c= the carrier of S2;

      let X be Subset of S1;

      thus X is Subset of S2 by A1, XBOOLE_1: 1;

      let X2 be Subset of S2 such that

       A2: X = X2;

      hereby

        assume

         A3: X is filtered;

        thus X2 is filtered

        proof

          let x,y be Element of S2;

          assume

           A4: x in X2 & y in X2;

          then

          reconsider x9 = x, y9 = y as Element of S1 by A2;

          consider z be Element of S1 such that

           A5: z in X and

           A6: z <= x9 & z <= y9 by A2, A3, A4;

          reconsider x1 = x, y1 = y, z1 = z as Element of L by YELLOW_0: 58;

          reconsider z as Element of S2 by A2, A5;

          take z;

          z1 <= x1 & z1 <= y1 by A6, YELLOW_0: 59;

          hence thesis by A2, A5, YELLOW_0: 60;

        end;

      end;

      assume

       A7: X is directed;

      let x,y be Element of S2;

      assume

       A8: x in X2 & y in X2;

      then

      reconsider x9 = x, y9 = y as Element of S1 by A2;

      consider z be Element of S1 such that

       A9: z in X and

       A10: x9 <= z & y9 <= z by A2, A7, A8;

      reconsider x1 = x, y1 = y, z1 = z as Element of L by YELLOW_0: 58;

      reconsider z as Element of S2 by A2, A9;

      take z;

      x1 <= z1 & y1 <= z1 by A10, YELLOW_0: 59;

      hence thesis by A2, A9, YELLOW_0: 60;

    end;

    begin

    definition

      let J be set, L be RelStr;

      let f,g be Function of J, the carrier of L;

      :: YELLOW_2:def1

      pred f <= g means for j be set st j in J holds ex a,b be Element of L st a = (f . j) & b = (g . j) & a <= b;

    end

    notation

      let J be set, L be RelStr;

      let f,g be Function of J, the carrier of L;

      synonym g >= f for f <= g;

    end

    theorem :: YELLOW_2:9

    for L,M be non empty RelStr, f,g be Function of L, M holds f <= g iff for x be Element of L holds (f . x) <= (g . x)

    proof

      let L,M be non empty RelStr, f,g be Function of L, M;

      hereby

        assume

         A1: f <= g;

        let x be Element of L;

        ex m1,m2 be Element of M st m1 = (f . x) & m2 = (g . x) & m1 <= m2 by A1;

        hence (f . x) <= (g . x);

      end;

      assume

       A2: for x be Element of L holds (f . x) <= (g . x);

      let x be set;

      assume x in the carrier of L;

      then

      reconsider x as Element of L;

      take (f . x), (g . x);

      thus thesis by A2;

    end;

    begin

    definition

      let L,M be non empty RelStr;

      let f be Function of L, M;

      :: YELLOW_2:def2

      func Image f -> strict full SubRelStr of M equals ( subrelstr ( rng f));

      correctness ;

    end

    theorem :: YELLOW_2:10

    for L,M be non empty RelStr holds for f be Function of L, M holds for y be Element of ( Image f) holds ex x be Element of L st (f . x) = y

    proof

      let L1,L2 be non empty RelStr, g be Function of L1, L2;

      let s be Element of ( Image g);

      ( dom g) = the carrier of L1 by FUNCT_2:def 1;

      then

       A1: ( rng g) is non empty by RELAT_1: 42;

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

      then

      consider l be object such that

       A2: l in ( dom g) and

       A3: s = (g . l) by A1, FUNCT_1:def 3;

      reconsider l as Element of L1 by A2;

      take l;

      thus thesis by A3;

    end;

    registration

      let L be non empty RelStr;

      let X be non empty Subset of L;

      cluster ( subrelstr X) -> non empty;

      coherence by YELLOW_0:def 15;

    end

    registration

      let L,M be non empty RelStr;

      let f be Function of L, M;

      cluster ( Image f) -> non empty;

      coherence

      proof

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

        then ( rng f) is non empty by RELAT_1: 42;

        hence thesis;

      end;

    end

    begin

    theorem :: YELLOW_2:11

    for L be non empty RelStr holds ( id L) is monotone

    proof

      let L be non empty RelStr;

      let l1,l2 be Element of L;

      assume l1 <= l2;

      then l1 <= (( id L) . l2) by FUNCT_1: 18;

      hence thesis by FUNCT_1: 18;

    end;

    theorem :: YELLOW_2:12

    for L,M,N be non empty RelStr holds for f be Function of L, M, g be Function of M, N holds f is monotone & g is monotone implies (g * f) is monotone

    proof

      let L1,L2,L3 be non empty RelStr;

      let g1 be Function of L1, L2, g2 be Function of L2, L3 such that

       A1: g1 is monotone and

       A2: g2 is monotone;

      let s1,s2 be Element of L1;

      assume s1 <= s2;

      then (g1 . s1) <= (g1 . s2) by A1;

      then (g2 . (g1 . s1)) <= (g2 . (g1 . s2)) by A2;

      then ((g2 * g1) . s1) <= (g2 . (g1 . s2)) by FUNCT_2: 15;

      hence thesis by FUNCT_2: 15;

    end;

    theorem :: YELLOW_2:13

    for L,M be non empty RelStr holds for f be Function of L, M holds for X be Subset of L, x be Element of L holds f is monotone & x is_<=_than X implies (f . x) is_<=_than (f .: X)

    proof

      let L1,L2 be non empty RelStr, g be Function of L1, L2;

      let X be Subset of L1, x be Element of L1 such that

       A1: g is monotone and

       A2: x is_<=_than X;

      let y2 be Element of L2;

      assume y2 in (g .: X);

      then

      consider x2 be Element of L1 such that

       A3: x2 in X and

       A4: y2 = (g . x2) by FUNCT_2: 65;

      reconsider x2 as Element of L1;

      x <= x2 by A2, A3;

      hence thesis by A1, A4;

    end;

    theorem :: YELLOW_2:14

    for L,M be non empty RelStr holds for f be Function of L, M holds for X be Subset of L, x be Element of L holds f is monotone & X is_<=_than x implies (f .: X) is_<=_than (f . x)

    proof

      let L1,L2 be non empty RelStr, g be Function of L1, L2;

      let X be Subset of L1, x be Element of L1 such that

       A1: g is monotone and

       A2: x is_>=_than X;

      let y2 be Element of L2;

      assume y2 in (g .: X);

      then

      consider x2 be Element of L1 such that

       A3: x2 in X and

       A4: y2 = (g . x2) by FUNCT_2: 65;

      reconsider x2 as Element of L1;

      x >= x2 by A2, A3;

      hence thesis by A1, A4;

    end;

    theorem :: YELLOW_2:15

    for S,T be non empty RelStr holds for f be Function of S, T holds for X be directed Subset of S holds f is monotone implies (f .: X) is directed

    proof

      let S,T be non empty RelStr;

      let f be Function of S, T;

      let X be directed Subset of S;

      set Y = (f .: X);

      assume

       A1: f is monotone;

      for y1,y2 be Element of T st y1 in Y & y2 in Y holds ex z be Element of T st z in Y & y1 <= z & y2 <= z

      proof

        let y1,y2 be Element of T;

        assume that

         A2: y1 in Y and

         A3: y2 in Y;

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

         A4: x1 in X and

         A5: y1 = (f . x1) by A2, FUNCT_1:def 6;

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

         A6: x2 in X and

         A7: y2 = (f . x2) by A3, FUNCT_1:def 6;

        reconsider x1, x2 as Element of S by A4, A6;

        consider z be Element of S such that

         A8: z in X and

         A9: x1 <= z & x2 <= z by A4, A6, WAYBEL_0:def 1;

        take (f . z);

        thus (f . z) in Y by A8, FUNCT_2: 35;

        thus thesis by A1, A5, A7, A9;

      end;

      hence thesis;

    end;

    theorem :: YELLOW_2:16



     Th16: for L be with_suprema Poset holds for f be Function of L, L holds f is directed-sups-preserving implies f is monotone

    proof

      let L be with_suprema Poset;

      let f be Function of L, L;

      assume

       A1: f is directed-sups-preserving;

      let x,y be Element of L such that

       A2: x <= y;



       A3: y = (y "\/" x) by A2, YELLOW_0: 24;

      for a,b be Element of L st a in {x, y} & b in {x, y} holds ex z be Element of L st z in {x, y} & a <= z & b <= z

      proof

        let a,b be Element of L such that

         A4: a in {x, y} & b in {x, y};

        take y;

        thus y in {x, y} by TARSKI:def 2;

        thus thesis by A2, A4, TARSKI:def 2;

      end;

      then {x, y} is directed non empty;

      then

       A5: f preserves_sup_of {x, y} by A1;



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

      y <= y;

      then

       A7: {x, y} is_<=_than y by A2, YELLOW_0: 8;

      for b be Element of L st {x, y} is_<=_than b holds y <= b by YELLOW_0: 8;

      then ex_sup_of ( {x, y},L) by A7, YELLOW_0: 30;



      then ( sup (f .: {x, y})) = (f . ( sup {x, y})) by A5

      .= (f . y) by A3, YELLOW_0: 41;



      then

       A8: (f . y) = ( sup {(f . x), (f . y)}) by A6, FUNCT_1: 60

      .= ((f . y) "\/" (f . x)) by YELLOW_0: 41;

      let afx,bfy be Element of L;

      assume afx = (f . x) & bfy = (f . y);

      hence afx <= bfy by A8, YELLOW_0: 22;

    end;

    theorem :: YELLOW_2:17

    for L be with_infima Poset holds for f be Function of L, L holds f is filtered-infs-preserving implies f is monotone

    proof

      let L be with_infima Poset;

      let f be Function of L, L;

      assume

       A1: f is filtered-infs-preserving;

      let x,y be Element of L such that

       A2: x <= y;



       A3: x = (x "/\" y) by A2, YELLOW_0: 25;

      for c,d be Element of L st c in {x, y} & d in {x, y} holds ex z be Element of L st z in {x, y} & z <= c & z <= d

      proof

        let c,d be Element of L such that

         A4: c in {x, y} & d in {x, y};

        take x;

        thus x in {x, y} by TARSKI:def 2;

        thus thesis by A2, A4, TARSKI:def 2;

      end;

      then {x, y} is filtered non empty;

      then

       A5: f preserves_inf_of {x, y} by A1;



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

      x <= x;

      then

       A7: x is_<=_than {x, y} by A2, YELLOW_0: 8;

      for c be Element of L st c is_<=_than {x, y} holds c <= x by YELLOW_0: 8;

      then ex_inf_of ( {x, y},L) by A7, YELLOW_0: 31;



      then ( inf (f .: {x, y})) = (f . ( inf {x, y})) by A5

      .= (f . x) by A3, YELLOW_0: 40;



      then

       A8: (f . x) = ( inf {(f . x), (f . y)}) by A6, FUNCT_1: 60

      .= ((f . x) "/\" (f . y)) by YELLOW_0: 40;

      let a,b be Element of L;

      assume a = (f . x) & b = (f . y);

      hence a <= b by A8, YELLOW_0: 23;

    end;

    begin

    theorem :: YELLOW_2:18

    for S be non empty 1-sorted holds for f be Function of S, S holds f is idempotent implies for x be Element of S holds (f . (f . x)) = (f . x)

    proof

      let L be non empty 1-sorted, p be Function of L, L;

      assume

       A1: (p * p) = p;

      let l be Element of L;

      thus thesis by A1, FUNCT_2: 15;

    end;

    theorem :: YELLOW_2:19



     Th19: for S be non empty 1-sorted holds for f be Function of S, S holds f is idempotent implies ( rng f) = { x where x be Element of S : x = (f . x) }

    proof

      let S be non empty 1-sorted;

      let f be Function of S, S;

      set M = { x where x be Element of S : x = (f . x) };

      assume

       A1: f = (f * f);



       A2: ( rng f) c= M

      proof

        let y be object;

        assume

         A3: y in ( rng f);

        then

        reconsider y9 = y as Element of S;

        ex x be object st x in ( dom f) & y = (f . x) by A3, FUNCT_1:def 3;

        then y9 = (f . y9) by A1, FUNCT_1: 13;

        hence thesis;

      end;

      M c= ( rng f)

      proof

        let y be object;

        assume y in M;

        then

         A4: ex y9 be Element of S st y9 = y & y9 = (f . y9);

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

        hence thesis by A4, FUNCT_1:def 3;

      end;

      hence thesis by A2, XBOOLE_0:def 10;

    end;

    theorem :: YELLOW_2:20



     Th20: for S be non empty 1-sorted holds for f be Function of S, S st f is idempotent holds X c= ( rng f) implies (f .: X) = X

    proof

      let S be non empty 1-sorted;

      let f be Function of S, S such that

       A1: f is idempotent;

      set M = { x where x be Element of S : x = (f . x) };

      assume X c= ( rng f);

      then

       A2: X c= M by A1, Th19;



       A3: (f .: X) c= X

      proof

        let y be object;

        assume y in (f .: X);

        then

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

         A4: x in X and

         A5: y = (f . x) by FUNCT_1:def 6;

        x in M by A2, A4;

        then ex x9 be Element of S st x9 = x & x9 = (f . x9);

        hence thesis by A4, A5;

      end;

      X c= (f .: X)

      proof

        let y be object;

        assume

         A6: y in X;

        then y in M by A2;

        then ex x be Element of S st x = y & x = (f . x);

        hence thesis by A6, FUNCT_2: 35;

      end;

      hence thesis by A3, XBOOLE_0:def 10;

    end;

    theorem :: YELLOW_2:21

    for L be non empty RelStr holds ( id L) is idempotent

    proof

      let L be non empty RelStr;



      thus (( id L) * ( id L)) = ( id (the carrier of L /\ the carrier of L)) by FUNCT_1: 22

      .= ( id L);

    end;

    begin

    reserve L for complete LATTICE,

a for Element of L;

    theorem :: YELLOW_2:22



     Th22: a in X implies a <= ( "\/" (X,L)) & ( "/\" (X,L)) <= a

    proof

      assume

       A1: a in X;

      X is_<=_than ( "\/" (X,L)) by YELLOW_0: 32;

      hence a <= ( "\/" (X,L)) by A1;

      X is_>=_than ( "/\" (X,L)) by YELLOW_0: 33;

      hence thesis by A1;

    end;

    theorem :: YELLOW_2:23



     Th23: for L be non empty RelStr holds (for X holds ex_sup_of (X,L)) iff (for Y holds ex_inf_of (Y,L))

    proof

      let L be non empty RelStr;

      hereby

        assume

         A1: for X holds ex_sup_of (X,L);

        let Y;

        set X = { x where x be Element of L : x is_<=_than Y };

         ex_sup_of (X,L) by A1;

        then

        consider a be Element of L such that

         A2: X is_<=_than a and

         A3: for b be Element of L st X is_<=_than b holds b >= a and

         A4: for c be Element of L st X is_<=_than c & for b be Element of L st X is_<=_than b holds b >= c holds c = a by YELLOW_0:def 7;



         A5: a is_<=_than Y

        proof

          let b be Element of L;

          assume

           A6: b in Y;

          b is_>=_than X

          proof

            let c be Element of L;

            assume c in X;

            then ex x be Element of L st c = x & x is_<=_than Y;

            hence thesis by A6;

          end;

          hence thesis by A3;

        end;



         A7: for c be Element of L st Y is_>=_than c & for b be Element of L st Y is_>=_than b holds b <= c holds c = a

        proof

          let c be Element of L such that

           A8: Y is_>=_than c and

           A9: for b be Element of L st Y is_>=_than b holds b <= c;



           A10: for b be Element of L st X is_<=_than b holds b >= c

          proof

            let b be Element of L;

            assume

             A11: X is_<=_than b;

            c in X by A8;

            hence thesis by A11;

          end;

          X is_<=_than c

          proof

            let b be Element of L;

            assume b in X;

            then ex x be Element of L st b = x & x is_<=_than Y;

            hence thesis by A9;

          end;

          hence thesis by A4, A10;

        end;

        for b be Element of L st Y is_>=_than b holds a >= b

        proof

          let b be Element of L;

          assume b is_<=_than Y;

          then b in X;

          hence thesis by A2;

        end;

        hence ex_inf_of (Y,L) by A5, A7, YELLOW_0:def 8;

      end;

      assume

       A12: for Y holds ex_inf_of (Y,L);

      let X;

      set Y = { y where y be Element of L : X is_<=_than y };

       ex_inf_of (Y,L) by A12;

      then

      consider a be Element of L such that

       A13: Y is_>=_than a and

       A14: for b be Element of L st Y is_>=_than b holds b <= a and

       A15: for c be Element of L st Y is_>=_than c & for b be Element of L st Y is_>=_than b holds b <= c holds c = a by YELLOW_0:def 8;



       A16: X is_<=_than a

      proof

        let b be Element of L;

        assume

         A17: b in X;

        b is_<=_than Y

        proof

          let c be Element of L;

          assume c in Y;

          then ex y be Element of L st c = y & X is_<=_than y;

          hence thesis by A17;

        end;

        hence thesis by A14;

      end;



       A18: for c be Element of L st X is_<=_than c & for b be Element of L st X is_<=_than b holds b >= c holds c = a

      proof

        let c be Element of L such that

         A19: X is_<=_than c and

         A20: for b be Element of L st X is_<=_than b holds b >= c;



         A21: for b be Element of L st Y is_>=_than b holds b <= c

        proof

          let b be Element of L;

          assume

           A22: Y is_>=_than b;

          c in Y by A19;

          hence thesis by A22;

        end;

        Y is_>=_than c

        proof

          let b be Element of L;

          assume b in Y;

          then ex x be Element of L st b = x & x is_>=_than X;

          hence thesis by A20;

        end;

        hence thesis by A15, A21;

      end;

      for b be Element of L st X is_<=_than b holds a <= b

      proof

        let b be Element of L;

        assume X is_<=_than b;

        then b in Y;

        hence thesis by A13;

      end;

      hence thesis by A16, A18, YELLOW_0:def 7;

    end;

    theorem :: YELLOW_2:24



     Th24: for L be non empty RelStr holds (for X holds ex_sup_of (X,L)) implies L is complete

    proof

      let L be non empty RelStr;

      assume

       A1: for X holds ex_sup_of (X,L);

      L is complete

      proof

        let X be set;

        take a = ( "\/" (X,L));



         A2: ex_sup_of (X,L) by A1;

        hence X is_<=_than a by YELLOW_0:def 9;

        thus thesis by A2, YELLOW_0:def 9;

      end;

      hence thesis;

    end;

    theorem :: YELLOW_2:25



     Th25: for L be non empty RelStr holds (for X holds ex_inf_of (X,L)) implies L is complete

    proof

      let L be non empty RelStr;

      assume for X holds ex_inf_of (X,L);

      then for X holds ex_sup_of (X,L) by Th23;

      hence thesis by Th24;

    end;

    theorem :: YELLOW_2:26



     Th26: for L be non empty RelStr holds (for A be Subset of L holds ex_inf_of (A,L)) implies for X holds ex_inf_of (X,L) & ( "/\" (X,L)) = ( "/\" ((X /\ the carrier of L),L))

    proof

      let L be non empty RelStr;

      assume

       A1: for A be Subset of L holds ex_inf_of (A,L);

      let X;

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

      set a = ( "/\" (Y,L));

      reconsider Y as Subset of L by XBOOLE_1: 17;



       A2: ex_inf_of (Y,L) by A1;



       A3: a is_<=_than X

      proof

        let x be Element of L;

        assume x in X;

        then

         A4: x in Y by XBOOLE_0:def 4;

        a is_<=_than Y by A2, YELLOW_0:def 10;

        hence thesis by A4;

      end;



       A5: for b be Element of L st b is_<=_than X holds b <= a

      proof

        let b be Element of L;



         A6: Y c= X by XBOOLE_1: 17;

        assume b is_<=_than X;

        then b is_<=_than Y by A6;

        hence thesis by A2, YELLOW_0:def 10;

      end;

       ex_inf_of (X,L) by A2, YELLOW_0: 50;

      hence thesis by A3, A5, YELLOW_0:def 10;

    end;

    theorem :: YELLOW_2:27

    for L be non empty RelStr holds (for A be Subset of L holds ex_sup_of (A,L)) implies for X holds ex_sup_of (X,L) & ( "\/" (X,L)) = ( "\/" ((X /\ the carrier of L),L))

    proof

      let L be non empty RelStr;

      assume

       A1: for A be Subset of L holds ex_sup_of (A,L);

      let X;

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

      set a = ( "\/" (Y,L));

      reconsider Y as Subset of L by XBOOLE_1: 17;



       A2: ex_sup_of (Y,L) by A1;



       A3: X is_<=_than a

      proof

        let x be Element of L;

        assume x in X;

        then

         A4: x in Y by XBOOLE_0:def 4;

        Y is_<=_than a by A2, YELLOW_0:def 9;

        hence thesis by A4;

      end;



       A5: for b be Element of L st X is_<=_than b holds a <= b

      proof

        let b be Element of L;



         A6: Y c= X by XBOOLE_1: 17;

        assume X is_<=_than b;

        then Y is_<=_than b by A6;

        hence thesis by A2, YELLOW_0:def 9;

      end;

       ex_sup_of (X,L) by A2, YELLOW_0: 50;

      hence thesis by A3, A5, YELLOW_0:def 9;

    end;

    theorem :: YELLOW_2:28



     Th28: for L be non empty RelStr holds (for A be Subset of L holds ex_inf_of (A,L)) implies L is complete

    proof

      let L be non empty RelStr;

      assume for A be Subset of L holds ex_inf_of (A,L);

      then for X holds ex_inf_of (X,L) by Th26;

      hence thesis by Th25;

    end;

    registration

      cluster up-complete /\-complete upper-bounded -> complete for non empty Poset;

      correctness ;

    end

    theorem :: YELLOW_2:29



     Th29: for f be Function of L, L st f is monotone holds for M be Subset of L st M = { x where x be Element of L : x = (f . x) } holds ( subrelstr M) is complete LATTICE

    proof

      let f be Function of L, L such that

       A1: f is monotone;

      let M be Subset of L such that

       A2: M = { x where x be Element of L : x = (f . x) };

      set S = ( subrelstr M);



       A3: for X be Subset of S holds for Y be Subset of L st Y = { y where y be Element of L : X is_<=_than (f . y) & (f . y) <= y } holds ( inf Y) in M

      proof

        let X be Subset of S;

        let Y be Subset of L such that

         A4: Y = { y where y be Element of L : X is_<=_than (f . y) & (f . y) <= y };

        set z = ( inf Y);



         A5: (f . z) is_<=_than Y

        proof

          let u be Element of L;

          assume

           A6: u in Y;

          then

          consider y be Element of L such that

           A7: y = u and X is_<=_than (f . y) and

           A8: (f . y) <= y by A4;

          z <= u by A6, Th22;

          then (f . z) <= (f . y) by A1, A7;

          hence (f . z) <= u by A7, A8, ORDERS_2: 3;

        end;



         A9: X is_<=_than (f . (f . z))

        proof

          let m be Element of L;

          assume

           A10: m in X;

          m is_<=_than Y

          proof

            let u be Element of L;

            assume u in Y;

            then

            consider y be Element of L such that

             A11: y = u and

             A12: X is_<=_than (f . y) and

             A13: (f . y) <= y by A4;

            m <= (f . y) by A10, A12;

            hence m <= u by A11, A13, ORDERS_2: 3;

          end;

          then m <= z by YELLOW_0: 33;

          then

           A14: (f . m) <= (f . z) by A1;

          X c= the carrier of S;

          then X c= M by YELLOW_0:def 15;

          then m in M by A10;

          then ex x be Element of L st x = m & x = (f . x) by A2;

          hence m <= (f . (f . z)) by A1, A14;

        end;

         ex_inf_of (Y,L) by YELLOW_0: 17;

        then

         A15: (f . z) <= z by A5, YELLOW_0: 31;

        then (f . (f . z)) <= (f . z) by A1;

        then (f . z) in Y by A4, A9;

        then z <= (f . z) by Th22;

        then z = (f . z) by A15, ORDERS_2: 2;

        hence thesis by A2;

      end;

      M c= the carrier of S by YELLOW_0:def 15;

      then

      reconsider M as Subset of S;

      defpred P[ Element of L] means M is_<=_than (f . $1) & (f . $1) <= $1;

      reconsider Y = { y where y be Element of L : P[y] } as Subset of L from DOMAIN_1:sch 7;

      ( inf Y) in M by A3;

      then

      reconsider S as non empty Poset;

      for X be Subset of S holds ex_sup_of (X,S)

      proof

        let X be Subset of S;

        defpred Q[ Element of L] means X is_<=_than (f . $1) & (f . $1) <= $1;

        reconsider Y = { y where y be Element of L : Q[y] } as Subset of L from DOMAIN_1:sch 7;

        set z = ( inf Y);

        z in M by A3;

        then

        reconsider z as Element of S;



         A16: X is_<=_than z

        proof

          let x be Element of S;

          x in the carrier of S;

          then x in M by YELLOW_0:def 15;

          then

          consider m be Element of L such that

           A17: x = m and m = (f . m) by A2;

          assume

           A18: x in X;

          m is_<=_than Y

          proof

            let u be Element of L;

            assume u in Y;

            then

            consider y be Element of L such that

             A19: y = u and

             A20: X is_<=_than (f . y) and

             A21: (f . y) <= y;

            m <= (f . y) by A18, A17, A20;

            hence m <= u by A19, A21, ORDERS_2: 3;

          end;

          then m <= ( inf Y) by YELLOW_0: 33;

          hence x <= z by A17, YELLOW_0: 60;

        end;

        for b be Element of S st X is_<=_than b holds z <= b

        proof

          let b be Element of S;

          b in the carrier of S;

          then b in M by YELLOW_0:def 15;

          then

          consider x be Element of L such that

           A22: x = b and

           A23: x = (f . x) by A2;

          assume X is_<=_than b;

          then X is_<=_than (f . x) by A22, A23, YELLOW_0: 62;

          then x in Y by A23;

          hence thesis by A22, Th22, YELLOW_0: 60;

        end;

        hence thesis by A16, YELLOW_0: 30;

      end;

      then

      reconsider S as complete non empty Poset by YELLOW_0: 53;

      S is complete LATTICE;

      hence thesis;

    end;

    theorem :: YELLOW_2:30



     Th30: for S be infs-inheriting non empty full SubRelStr of L holds S is complete LATTICE

    proof

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

      for X be Subset of S holds ex_inf_of (X,S)

      proof

        let X be Subset of S;



         A1: ex_inf_of (X,L) by YELLOW_0: 17;

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

        hence thesis by A1, YELLOW_0: 63;

      end;

      then S is complete by Th28;

      hence thesis;

    end;

    theorem :: YELLOW_2:31



     Th31: for S be sups-inheriting non empty full SubRelStr of L holds S is complete LATTICE

    proof

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

      for X be Subset of S holds ex_sup_of (X,S)

      proof

        let X be Subset of S;



         A1: ex_sup_of (X,L) by YELLOW_0: 17;

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

        hence thesis by A1, YELLOW_0: 64;

      end;

      then S is complete by YELLOW_0: 53;

      hence thesis;

    end;

    theorem :: YELLOW_2:32



     Th32: for M be non empty RelStr holds for f be Function of L, M st f is sups-preserving holds ( Image f) is sups-inheriting

    proof

      let M be non empty RelStr;

      let f be Function of L, M such that

       A1: f is sups-preserving;

      set S = ( subrelstr ( rng f));

      for Y be Subset of S st ex_sup_of (Y,M) holds ( "\/" (Y,M)) in the carrier of S

      proof

        let Y be Subset of S;

        assume ex_sup_of (Y,M);



         A2: f preserves_sup_of (f " Y) & ex_sup_of ((f " Y),L) by A1, YELLOW_0: 17;

        Y c= the carrier of S;

        then Y c= ( rng f) by YELLOW_0:def 15;



        then ( "\/" (Y,M)) = ( sup (f .: (f " Y))) by FUNCT_1: 77

        .= (f . ( sup (f " Y))) by A2;

        then ( "\/" (Y,M)) in ( rng f) by FUNCT_2: 4;

        hence thesis by YELLOW_0:def 15;

      end;

      hence thesis by YELLOW_0:def 19;

    end;

    theorem :: YELLOW_2:33



     Th33: for M be non empty RelStr holds for f be Function of L, M st f is infs-preserving holds ( Image f) is infs-inheriting

    proof

      let M be non empty RelStr;

      let f be Function of L, M such that

       A1: f is infs-preserving;

      set S = ( subrelstr ( rng f));

      for Y be Subset of S st ex_inf_of (Y,M) holds ( "/\" (Y,M)) in the carrier of S

      proof

        let Y be Subset of S;

        assume ex_inf_of (Y,M);



         A2: f preserves_inf_of (f " Y) & ex_inf_of ((f " Y),L) by A1, YELLOW_0: 17;

        Y c= the carrier of S;

        then Y c= ( rng f) by YELLOW_0:def 15;



        then ( "/\" (Y,M)) = ( inf (f .: (f " Y))) by FUNCT_1: 77

        .= (f . ( inf (f " Y))) by A2;

        then ( "/\" (Y,M)) in ( rng f) by FUNCT_2: 4;

        hence thesis by YELLOW_0:def 15;

      end;

      hence thesis by YELLOW_0:def 18;

    end;

    theorem :: YELLOW_2:34

    for L,M be complete LATTICE holds for f be Function of L, M st f is sups-preserving or f is infs-preserving holds ( Image f) is complete LATTICE

    proof

      let L,M be complete LATTICE;

      let f be Function of L, M such that

       A1: f is sups-preserving or f is infs-preserving;

      per cases by A1;

        suppose f is sups-preserving;

        then ( Image f) is sups-inheriting by Th32;

        hence thesis by Th31;

      end;

        suppose f is infs-preserving;

        then ( Image f) is infs-inheriting by Th33;

        hence thesis by Th30;

      end;

    end;

    theorem :: YELLOW_2:35

    for f be Function of L, L st f is idempotent directed-sups-preserving holds ( Image f) is directed-sups-inheriting & ( Image f) is complete LATTICE

    proof

      let f be Function of L, L;

      set S = ( subrelstr ( rng f));

      set a = the Element of L;

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

      then (f . a) in ( rng f) by FUNCT_1:def 3;

      then

      reconsider S9 = S as non empty full SubRelStr of L;

      assume

       A1: f is idempotent directed-sups-preserving;

      for X be directed Subset of S st X <> {} & ex_sup_of (X,L) holds ( "\/" (X,L)) in the carrier of S

      proof

        let X be directed Subset of S;

        X c= the carrier of S;

        then

         A2: X c= ( rng f) by YELLOW_0:def 15;

        assume X <> {} ;

        then X is non empty directed Subset of S9;

        then

        reconsider X9 = X as non empty directed Subset of L by Th7;

        assume

         A3: ex_sup_of (X,L);

        f preserves_sup_of X9 by A1;

        then ( sup (f .: X9)) = (f . ( sup X9)) by A3;

        then ( sup X9) = (f . ( sup X9)) by A1, A2, Th20;

        then ( "\/" (X,L)) in ( rng f) by FUNCT_2: 4;

        hence thesis by YELLOW_0:def 15;

      end;

      hence ( Image f) is directed-sups-inheriting;

      ( rng f) = { x where x be Element of L : x = (f . x) } by A1, Th19;

      hence thesis by A1, Th16, Th29;

    end;

    begin

    theorem :: YELLOW_2:36



     Th36: for L be RelStr holds for F be Subset-Family of L st for X be Subset of L st X in F holds X is lower holds ( meet F) is lower Subset of L

    proof

      let L be RelStr;

      let F be Subset-Family of L;

      reconsider F9 = F as Subset-Family of L;

      assume

       A1: for X be Subset of L st X in F holds X is lower;

      reconsider M = ( meet F9) as Subset of L;

      per cases ;

        suppose F = {} ;

        then for x,y be Element of L st x in M & y <= x holds y in M by SETFAM_1:def 1;

        hence thesis by WAYBEL_0:def 19;

      end;

        suppose

         A2: F <> {} ;

        for x,y be Element of L st x in M & y <= x holds y in M

        proof

          let x,y be Element of L;

          assume that

           A3: x in M and

           A4: y <= x;

          for Y be set st Y in F holds y in Y

          proof

            let Y be set;

            assume

             A5: Y in F;

            then

            reconsider X = Y as Subset of L;

            X is lower & x in X by A1, A3, A5, SETFAM_1:def 1;

            hence thesis by A4;

          end;

          hence thesis by A2, SETFAM_1:def 1;

        end;

        hence thesis by WAYBEL_0:def 19;

      end;

    end;

    theorem :: YELLOW_2:37

    for L be RelStr holds for F be Subset-Family of L st for X be Subset of L st X in F holds X is upper holds ( meet F) is upper Subset of L

    proof

      let L be RelStr;

      let F be Subset-Family of L;

      reconsider F9 = F as Subset-Family of L;

      assume

       A1: for X be Subset of L st X in F holds X is upper;

      reconsider M = ( meet F9) as Subset of L;

      per cases ;

        suppose F = {} ;

        then for x,y be Element of L st x in M & x <= y holds y in M by SETFAM_1:def 1;

        hence thesis by WAYBEL_0:def 20;

      end;

        suppose

         A2: F <> {} ;

        for x,y be Element of L st x in M & x <= y holds y in M

        proof

          let x,y be Element of L;

          assume that

           A3: x in M and

           A4: x <= y;

          for Y be set st Y in F holds y in Y

          proof

            let Y be set;

            assume

             A5: Y in F;

            then

            reconsider X = Y as Subset of L;

            X is upper & x in X by A1, A3, A5, SETFAM_1:def 1;

            hence thesis by A4;

          end;

          hence thesis by A2, SETFAM_1:def 1;

        end;

        hence thesis by WAYBEL_0:def 20;

      end;

    end;

    theorem :: YELLOW_2:38



     Th38: for L be with_suprema antisymmetric RelStr holds for F be Subset-Family of L st for X be Subset of L st X in F holds X is lower directed holds ( meet F) is directed Subset of L

    proof

      let L be with_suprema antisymmetric RelStr;

      let F be Subset-Family of L;

      assume

       A1: for X be Subset of L st X in F holds X is lower directed;

      reconsider F9 = F as Subset-Family of L;

      reconsider M = ( meet F9) as Subset of L;

      per cases ;

        suppose

         A2: F = {} ;

        M is directed by A2, SETFAM_1:def 1;

        hence thesis;

      end;

        suppose

         A3: F <> {} ;

        M is directed

        proof

          let x,y be Element of L such that

           A4: x in M and

           A5: y in M;

          take z = (x "\/" y);

          for Y be set st Y in F holds z in Y

          proof

            let Y be set;

            assume

             A6: Y in F;

            then

            reconsider X = Y as Subset of L;



             A7: y in X by A5, A6, SETFAM_1:def 1;

            X is lower directed & x in X by A1, A4, A6, SETFAM_1:def 1;

            hence thesis by A7, WAYBEL_0: 40;

          end;

          hence z in M by A3, SETFAM_1:def 1;

          thus thesis by YELLOW_0: 22;

        end;

        hence thesis;

      end;

    end;

    theorem :: YELLOW_2:39

    for L be with_infima antisymmetric RelStr holds for F be Subset-Family of L st for X be Subset of L st X in F holds X is upper filtered holds ( meet F) is filtered Subset of L

    proof

      let L be with_infima antisymmetric RelStr;

      let F be Subset-Family of L;

      assume

       A1: for X be Subset of L st X in F holds X is upper filtered;

      reconsider F9 = F as Subset-Family of L;

      reconsider M = ( meet F9) as Subset of L;

      per cases ;

        suppose

         A2: F = {} ;

        M is filtered by A2, SETFAM_1:def 1;

        hence thesis;

      end;

        suppose

         A3: F <> {} ;

        M is filtered

        proof

          let x,y be Element of L such that

           A4: x in M and

           A5: y in M;

          take z = (x "/\" y);

          for Y be set st Y in F holds z in Y

          proof

            let Y be set;

            assume

             A6: Y in F;

            then

            reconsider X = Y as Subset of L;



             A7: y in X by A5, A6, SETFAM_1:def 1;

            X is upper filtered & x in X by A1, A4, A6, SETFAM_1:def 1;

            hence thesis by A7, WAYBEL_0: 41;

          end;

          hence z in M by A3, SETFAM_1:def 1;

          thus thesis by YELLOW_0: 23;

        end;

        hence thesis;

      end;

    end;

    theorem :: YELLOW_2:40



     Th40: for L be with_infima Poset holds for I,J be Ideal of L holds (I /\ J) is Ideal of L

    proof

      let L be with_infima Poset;

      let I,J be Ideal of L;

      set i = the Element of I, j = the Element of J;

      set a = (i "/\" j);

      a <= j by YELLOW_0: 23;

      then

       A1: a in J by WAYBEL_0:def 19;

      a <= i by YELLOW_0: 23;

      then a in I by WAYBEL_0:def 19;

      hence thesis by A1, WAYBEL_0: 27, WAYBEL_0: 44, XBOOLE_0:def 4;

    end;

    registration

      let L be non empty reflexive transitive RelStr;

      cluster ( Ids L) -> non empty;

      correctness

      proof

        set x = the Element of L;

        ( downarrow x) in the set of all Y where Y be Ideal of L;

        hence thesis;

      end;

    end

    theorem :: YELLOW_2:41



     Th41: for L be non empty reflexive transitive RelStr holds (x is Element of ( InclPoset ( Ids L)) iff x is Ideal of L)

    proof

      let L be non empty reflexive transitive RelStr;

      hereby

        assume x is Element of ( InclPoset ( Ids L));

        then x in the carrier of ( InclPoset ( Ids L));

        then x in ( Ids L) by YELLOW_1: 1;

        then ex J be Ideal of L st J = x;

        hence x is Ideal of L;

      end;

      assume x is Ideal of L;

      then x in the set of all Y where Y be Ideal of L;

      hence thesis by YELLOW_1: 1;

    end;

    theorem :: YELLOW_2:42



     Th42: for L be non empty reflexive transitive RelStr holds for I be Element of ( InclPoset ( Ids L)) holds x in I implies x is Element of L

    proof

      let L be non empty reflexive transitive RelStr;

      let I be Element of ( InclPoset ( Ids L));

      reconsider I9 = I as non empty Subset of L by Th41;

      assume x in I;

      then

      reconsider x9 = x as Element of I9;

      x9 in the carrier of L;

      hence thesis;

    end;

    theorem :: YELLOW_2:43

    for L be with_infima Poset holds for x,y be Element of ( InclPoset ( Ids L)) holds (x "/\" y) = (x /\ y)

    proof

      let L be with_infima Poset;

      let x,y be Element of ( InclPoset ( Ids L));

      reconsider x9 = x, y9 = y as Ideal of L by Th41;

      (x9 /\ y9) is Ideal of L by Th40;

      then (x9 /\ y9) in the set of all X where X be Ideal of L;

      hence thesis by YELLOW_1: 9;

    end;

    registration

      let L be with_infima Poset;

      cluster ( InclPoset ( Ids L)) -> with_infima;

      correctness

      proof

        for x,y be set st x in ( Ids L) & y in ( Ids L) holds (x /\ y) in ( Ids L)

        proof

          let x,y be set;

          assume that

           A1: x in ( Ids L) and

           A2: y in ( Ids L);

          consider I be Ideal of L such that

           A3: I = x by A1;

          consider J be Ideal of L such that

           A4: J = y by A2;

          (I /\ J) is Ideal of L by Th40;

          hence thesis by A3, A4;

        end;

        hence thesis by YELLOW_1: 12;

      end;

    end

    theorem :: YELLOW_2:44



     Th44: for L be with_suprema Poset holds for x,y be Element of ( InclPoset ( Ids L)) holds ex Z be Subset of L st Z = { z where z be Element of L : z in x or z in y or ex a,b be Element of L st a in x & b in y & z = (a "\/" b) } & ex_sup_of ( {x, y},( InclPoset ( Ids L))) & (x "\/" y) = ( downarrow Z)

    proof

      let L be with_suprema Poset;

      set P = ( InclPoset ( Ids L));

      let x,y be Element of P;

      defpred P[ Element of L] means $1 in x or $1 in y or ex a,b be Element of L st a in x & b in y & $1 = (a "\/" b);

      reconsider Z = { z where z be Element of L : P[z] } as Subset of L from DOMAIN_1:sch 7;

      take Z;

      reconsider x9 = x, y9 = y as Ideal of L by Th41;

      set z = the Element of x9;

      z in Z;

      then

      reconsider Z as non empty Subset of L;

      set DZ = ( downarrow Z);

      for u,v be Element of L st u in Z & v in Z holds ex z be Element of L st z in Z & u <= z & v <= z

      proof



         A1: for p,q be Element of L st p in y & ex a,b be Element of L st a in x & b in y & q = (a "\/" b) holds ex z be Element of L st z in Z & p <= z & q <= z

        proof

          let p,q be Element of L such that

           A2: p in y and

           A3: ex a,b be Element of L st a in x & b in y & q = (a "\/" b);

          consider a,b be Element of L such that

           A4: a in x and

           A5: b in y and

           A6: q = (a "\/" b) by A3;

          reconsider c = (b "\/" p) as Element of L;

          take z = (a "\/" c);

          c in y9 by A2, A5, WAYBEL_0: 40;

          hence z in Z by A4;



           A7: c <= z by YELLOW_0: 22;



           A8: p <= c & a <= z by YELLOW_0: 22;

          b <= c by YELLOW_0: 22;

          then b <= z by A7, ORDERS_2: 3;

          hence thesis by A6, A7, A8, ORDERS_2: 3, YELLOW_0: 22;

        end;



         A9: for p,q be Element of L st p in x & ex a,b be Element of L st a in x & b in y & q = (a "\/" b) holds ex z be Element of L st z in Z & p <= z & q <= z

        proof

          let p,q be Element of L such that

           A10: p in x and

           A11: ex a,b be Element of L st a in x & b in y & q = (a "\/" b);

          consider a,b be Element of L such that

           A12: a in x and

           A13: b in y and

           A14: q = (a "\/" b) by A11;

          reconsider c = (a "\/" p) as Element of L;

          take z = (c "\/" b);

          c in x9 by A10, A12, WAYBEL_0: 40;

          hence z in Z by A13;



           A15: c <= z by YELLOW_0: 22;



           A16: p <= c & b <= z by YELLOW_0: 22;

          a <= c by YELLOW_0: 22;

          then a <= z by A15, ORDERS_2: 3;

          hence thesis by A14, A15, A16, ORDERS_2: 3, YELLOW_0: 22;

        end;

        let u,v be Element of L such that

         A17: u in Z and

         A18: v in Z;

        consider p be Element of L such that

         A19: p = u and

         A20: p in x or p in y or ex a,b be Element of L st a in x & b in y & p = (a "\/" b) by A17;

        consider q be Element of L such that

         A21: q = v and

         A22: q in x or q in y or ex a,b be Element of L st a in x & b in y & q = (a "\/" b) by A18;

        per cases by A20, A22;

          suppose p in x & q in x;

          then

          consider z be Element of L such that

           A23: z in x9 & p <= z & q <= z by WAYBEL_0:def 1;

          take z;

          thus thesis by A19, A21, A23;

        end;

          suppose

           A24: p in x & q in y;

          take (p "\/" q);

          thus thesis by A19, A21, A24, YELLOW_0: 22;

        end;

          suppose p in x & ex a,b be Element of L st a in x & b in y & q = (a "\/" b);

          then

          consider z be Element of L such that

           A25: z in Z & p <= z & q <= z by A9;

          take z;

          thus thesis by A19, A21, A25;

        end;

          suppose

           A26: p in y & q in x;

          take (q "\/" p);

          thus thesis by A19, A21, A26, YELLOW_0: 22;

        end;

          suppose p in y & q in y;

          then

          consider z be Element of L such that

           A27: z in y9 & p <= z & q <= z by WAYBEL_0:def 1;

          take z;

          thus thesis by A19, A21, A27;

        end;

          suppose p in y & ex a,b be Element of L st a in x & b in y & q = (a "\/" b);

          then

          consider z be Element of L such that

           A28: z in Z & p <= z & q <= z by A1;

          take z;

          thus thesis by A19, A21, A28;

        end;

          suppose q in x & ex a,b be Element of L st a in x & b in y & p = (a "\/" b);

          then

          consider z be Element of L such that

           A29: z in Z & q <= z & p <= z by A9;

          take z;

          thus thesis by A19, A21, A29;

        end;

          suppose q in y & ex a,b be Element of L st a in x & b in y & p = (a "\/" b);

          then

          consider z be Element of L such that

           A30: z in Z & q <= z & p <= z by A1;

          take z;

          thus thesis by A19, A21, A30;

        end;

          suppose (ex a,b be Element of L st a in x & b in y & p = (a "\/" b)) & ex a,b be Element of L st a in x & b in y & q = (a "\/" b);

          then

          consider a,b,c,d be Element of L such that

           A31: a in x & b in y and

           A32: p = (a "\/" b) and

           A33: c in x & d in y and

           A34: q = (c "\/" d);

          reconsider ac = (a "\/" c), bd = (b "\/" d) as Element of L;

          take z = (ac "\/" bd);

          ac in x9 & bd in y9 by A31, A33, WAYBEL_0: 40;

          hence z in Z;



           A35: ac <= z by YELLOW_0: 22;



           A36: bd <= z by YELLOW_0: 22;

          b <= bd by YELLOW_0: 22;

          then

           A37: b <= z by A36, ORDERS_2: 3;

          a <= ac by YELLOW_0: 22;

          then a <= z by A35, ORDERS_2: 3;

          hence u <= z by A19, A32, A37, YELLOW_0: 22;

          d <= bd by YELLOW_0: 22;

          then

           A38: d <= z by A36, ORDERS_2: 3;

          c <= ac by YELLOW_0: 22;

          then c <= z by A35, ORDERS_2: 3;

          hence thesis by A21, A34, A38, YELLOW_0: 22;

        end;

      end;

      then Z is directed;

      then

      reconsider DZ as Element of P by Th41;



       A39: for d be Element of P st d >= x & d >= y holds DZ <= d

      proof

        let d be Element of P;

        assume that

         A40: x <= d and

         A41: y <= d;



         A42: y c= d by A41, YELLOW_1: 3;



         A43: x c= d by A40, YELLOW_1: 3;

        DZ c= d

        proof

          let p be object;

          assume p in DZ;

          then p in { q where q be Element of L : ex u be Element of L st q <= u & u in Z } by WAYBEL_0: 14;

          then

          consider p9 be Element of L such that

           A44: p9 = p and

           A45: ex u be Element of L st p9 <= u & u in Z;

          consider u be Element of L such that

           A46: p9 <= u and

           A47: u in Z by A45;

          consider z be Element of L such that

           A48: z = u and

           A49: z in x or z in y or ex a,b be Element of L st a in x & b in y & z = (a "\/" b) by A47;

          per cases by A49;

            suppose z in x;

            then p in x9 by A44, A46, A48, WAYBEL_0:def 19;

            hence thesis by A43;

          end;

            suppose z in y;

            then p in y9 by A44, A46, A48, WAYBEL_0:def 19;

            hence thesis by A42;

          end;

            suppose

             A50: ex a,b be Element of L st a in x & b in y & z = (a "\/" b);

            reconsider d9 = d as Ideal of L by Th41;

            u in d9 by A43, A42, A48, A50, WAYBEL_0: 40;

            hence thesis by A44, A46, WAYBEL_0:def 19;

          end;

        end;

        hence thesis by YELLOW_1: 3;

      end;

      y c= DZ

      proof

        let a be object;



         A51: Z c= DZ by WAYBEL_0: 16;

        assume

         A52: a in y;

        then

        reconsider a9 = a as Element of L by Th42;

        a9 in Z by A52;

        hence thesis by A51;

      end;

      then

       A53: y <= DZ by YELLOW_1: 3;

      x c= DZ

      proof

        let a be object;



         A54: Z c= DZ by WAYBEL_0: 16;

        assume

         A55: a in x;

        then

        reconsider a9 = a as Element of L by Th42;

        a9 in Z by A55;

        hence thesis by A54;

      end;

      then x <= DZ by YELLOW_1: 3;

      hence thesis by A53, A39, YELLOW_0: 18;

    end;

    registration

      let L be with_suprema Poset;

      cluster ( InclPoset ( Ids L)) -> with_suprema;

      correctness

      proof

        set P = ( InclPoset ( Ids L));

        for x,y be Element of P holds ex z be Element of P st x <= z & y <= z & for z9 be Element of P st x <= z9 & y <= z9 holds z <= z9

        proof

          let x,y be Element of P;

          take (x "\/" y);

          ex Z be Subset of L st Z = { z where z be Element of L : z in x or z in y or ex a,b be Element of L st a in x & b in y & z = (a "\/" b) } & ex_sup_of ( {x, y},( InclPoset ( Ids L))) & (x "\/" y) = ( downarrow Z) by Th44;

          hence thesis by YELLOW_0: 18;

        end;

        hence thesis;

      end;

    end

    theorem :: YELLOW_2:45



     Th45: for L be lower-bounded sup-Semilattice holds for X be non empty Subset of ( Ids L) holds ( meet X) is Ideal of L

    proof

      let L be lower-bounded sup-Semilattice;

      let X be non empty Subset of ( Ids L);



       A1: for J be set st J in X holds J is Ideal of L

      proof

        let J be set;

        assume J in X;

        then J in ( Ids L);

        then ex Y be Ideal of L st Y = J;

        hence thesis;

      end;

      X c= ( bool the carrier of L)

      proof

        let x be object;

        assume x in X;

        then x is Ideal of L by A1;

        hence thesis;

      end;

      then

      reconsider F = X as Subset-Family of L;

      for J be Subset of L st J in F holds J is lower by A1;

      then

      reconsider I = ( meet X) as lower Subset of L by Th36;

      for J be set st J in X holds ( Bottom L) in J

      proof

        let J be set;

        assume J in X;

        then

        reconsider J9 = J as Ideal of L by A1;

        set j = the Element of J9;

        ( Bottom L) <= j by YELLOW_0: 44;

        hence thesis by WAYBEL_0:def 19;

      end;

      then

      reconsider I as non empty lower Subset of L by SETFAM_1:def 1;

      for J be Subset of L st J in F holds J is lower directed by A1;

      then I is Ideal of L by Th38;

      hence thesis;

    end;

    theorem :: YELLOW_2:46



     Th46: for L be lower-bounded sup-Semilattice holds for A be non empty Subset of ( InclPoset ( Ids L)) holds ex_inf_of (A,( InclPoset ( Ids L))) & ( inf A) = ( meet A)

    proof

      let L be lower-bounded sup-Semilattice;

      let A be non empty Subset of ( InclPoset ( Ids L));

      set P = ( InclPoset ( Ids L));

      reconsider A9 = A as non empty Subset of ( Ids L) by YELLOW_1: 1;

      ( meet A9) is Ideal of L by Th45;

      then

      reconsider I = ( meet A) as Element of P by Th41;



       A1: for b be Element of P st b is_<=_than A holds I >= b

      proof

        let b be Element of P;

        assume

         A2: A is_>=_than b;



         A3: for J be set st J in A holds b c= J by A2, YELLOW_1: 3;

        b c= I

        proof

          let c be object;

          assume

           A4: c in b;

          for J be set st J in A holds c in J

          proof

            let J be set;

            assume J in A;

            then b c= J by A3;

            hence thesis by A4;

          end;

          hence thesis by SETFAM_1:def 1;

        end;

        hence thesis by YELLOW_1: 3;

      end;

      I is_<=_than A

      proof

        let y be Element of P;

        assume

         A5: y in A;

        I c= y by A5, SETFAM_1:def 1;

        hence I <= y by YELLOW_1: 3;

      end;

      hence thesis by A1, YELLOW_0: 31;

    end;

    theorem :: YELLOW_2:47



     Th47: for L be with_suprema Poset holds ex_inf_of ( {} ,( InclPoset ( Ids L))) & ( "/\" ( {} ,( InclPoset ( Ids L)))) = ( [#] L)

    proof

      let L be with_suprema Poset;

      set P = ( InclPoset ( Ids L));

      reconsider I = ( [#] L) as Element of P by Th41;



       A1: for b be Element of P st b is_<=_than {} holds I >= b

      proof

        let b be Element of P;

        reconsider b9 = b as Ideal of L by Th41;

        assume {} is_>=_than b;

        b9 c= ( [#] L);

        hence thesis by YELLOW_1: 3;

      end;

      I is_<=_than {} ;

      hence thesis by A1, YELLOW_0: 31;

    end;

    theorem :: YELLOW_2:48



     Th48: for L be lower-bounded sup-Semilattice holds ( InclPoset ( Ids L)) is complete

    proof

      let L be lower-bounded sup-Semilattice;

      set P = ( InclPoset ( Ids L));

      for A be Subset of P holds ex_inf_of (A,( InclPoset ( Ids L)))

      proof

        let A be Subset of P;

        per cases ;

          suppose A = {} ;

          hence thesis by Th47;

        end;

          suppose A <> {} ;

          hence thesis by Th46;

        end;

      end;

      hence thesis by Th28;

    end;

    registration

      let L be lower-bounded sup-Semilattice;

      cluster ( InclPoset ( Ids L)) -> complete;

      correctness by Th48;

    end

    begin

    definition

      let L be non empty Poset;

      :: YELLOW_2:def3

      func SupMap L -> Function of ( InclPoset ( Ids L)), L means

      : Def3: for I be Ideal of L holds (it . I) = ( sup I);

      existence

      proof

        deffunc F( set) = ( "\/" ($1,L));

        set P = ( InclPoset ( Ids L));



         A1: for I be set st I in the carrier of P holds F(I) in the carrier of L;

        ex f be Function of the carrier of P, the carrier of L st for I be set st I in the carrier of P holds (f . I) = F(I) from FUNCT_2:sch 11( A1);

        then

        consider f be Function of the carrier of P, the carrier of L such that

         A2: for I be set st I in the carrier of P holds (f . I) = ( "\/" (I,L));

        reconsider f as Function of P, L;

        take f;

        for I be Ideal of L holds (f . I) = ( sup I)

        proof

          let I be Ideal of L;

          I in the carrier of RelStr (# ( Ids L), ( RelIncl ( Ids L)) #);

          then I in the carrier of P by YELLOW_1:def 1;

          hence thesis by A2;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        set P = ( InclPoset ( Ids L));

        let f,g be Function of ( InclPoset ( Ids L)), L;

        assume that

         A3: for I be Ideal of L holds (f . I) = ( sup I) and

         A4: for I be Ideal of L holds (g . I) = ( sup I);



         A5: the carrier of P = the carrier of RelStr (# ( Ids L), ( RelIncl ( Ids L)) #) by YELLOW_1:def 1

        .= ( Ids L);

         A6:

        now

          let x be object;

          assume x in the carrier of P;

          then ex I be Ideal of L st x = I by A5;

          then

          reconsider I = x as Ideal of L;

          (f . I) = ( sup I) by A3;

          hence (f . x) = (g . x) by A4;

        end;

        ( dom f) = the carrier of P & ( dom g) = the carrier of P by FUNCT_2:def 1;

        hence f = g by A6, FUNCT_1: 2;

      end;

    end

    theorem :: YELLOW_2:49



     Th49: for L be non empty Poset holds ( dom ( SupMap L)) = ( Ids L) & ( rng ( SupMap L)) is Subset of L

    proof

      let L be non empty Poset;

      set P = ( InclPoset ( Ids L));



      thus ( dom ( SupMap L)) = the carrier of P by FUNCT_2:def 1

      .= the carrier of RelStr (# ( Ids L), ( RelIncl ( Ids L)) #) by YELLOW_1:def 1

      .= ( Ids L);

      thus thesis;

    end;

    theorem :: YELLOW_2:50

    for L be non empty Poset holds x in ( dom ( SupMap L)) iff x is Ideal of L

    proof

      let L be non empty Poset;

      hereby

        assume x in ( dom ( SupMap L));

        then x in ( Ids L) by Th49;

        then ex I be Ideal of L st x = I;

        hence x is Ideal of L;

      end;

      assume x is Ideal of L;

      then x in the set of all X where X be Ideal of L;

      hence thesis by Th49;

    end;

    theorem :: YELLOW_2:51



     Th51: for L be up-complete non empty Poset holds ( SupMap L) is monotone

    proof

      let L be up-complete non empty Poset;

      set P = ( InclPoset ( Ids L));

      set f = ( SupMap L);

      for x,y be Element of P st x <= y holds for a,b be Element of L st a = (f . x) & b = (f . y) holds a <= b

      proof

        let x,y be Element of P such that

         A1: x <= y;

        reconsider I = x, J = y as Ideal of L by Th41;



         A2: I c= J by A1, YELLOW_1: 3;



         A3: ex_sup_of (I,L) & ex_sup_of (J,L) by WAYBEL_0: 75;



         A4: (f . x) = ( sup I) & (f . y) = ( sup J) by Def3;

        let a,b be Element of L;

        assume a = (f . x) & b = (f . y);

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

      end;

      hence thesis;

    end;

    registration

      let L be up-complete non empty Poset;

      cluster ( SupMap L) -> monotone;

      correctness by Th51;

    end

    definition

      let L be non empty Poset;

      :: YELLOW_2:def4

      func IdsMap L -> Function of L, ( InclPoset ( Ids L)) means

      : Def4: for x be Element of L holds (it . x) = ( downarrow x);

      existence

      proof

        deffunc F( Element of L) = ( downarrow $1);



         A1: for x be Element of L holds F(x) is Element of ( InclPoset ( Ids L)) by Th41;

        thus ex m be Function of L, ( InclPoset ( Ids L)) st for x be Element of L holds (m . x) = F(x) from FUNCT_2:sch 9( A1);

      end;

      uniqueness

      proof

        let f1,f2 be Function of L, ( InclPoset ( Ids L)) such that

         A2: for x be Element of L holds (f1 . x) = ( downarrow x) and

         A3: for x be Element of L holds (f2 . x) = ( downarrow x);

        now

          let x be Element of L;



          thus (f1 . x) = ( downarrow x) by A2

          .= (f2 . x) by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: YELLOW_2:52



     Th52: for L be non empty Poset holds ( IdsMap L) is monotone

    proof

      let L be non empty Poset;

      let x1,x2 be Element of L;

      assume x1 <= x2;

      then ( downarrow x1) c= ( downarrow x2) by WAYBEL_0: 21;

      then (( IdsMap L) . x1) c= ( downarrow x2) by Def4;

      then

       A1: (( IdsMap L) . x1) c= (( IdsMap L) . x2) by Def4;

      let a,b be Element of ( InclPoset ( Ids L));

      assume a = (( IdsMap L) . x1) & b = (( IdsMap L) . x2);

      hence a <= b by A1, YELLOW_1: 3;

    end;

    registration

      let L be non empty Poset;

      cluster ( IdsMap L) -> monotone;

      correctness by Th52;

    end

    begin

    definition

      let L be non empty RelStr;

      let F be Relation;

      :: YELLOW_2:def5

      func \\/ (F,L) -> Element of L equals ( "\/" (( rng F),L));

      coherence ;

      :: YELLOW_2:def6

      func //\ (F,L) -> Element of L equals ( "/\" (( rng F),L));

      coherence ;

    end

    notation

      let J be set, L be non empty RelStr;

      let F be Function of J, the carrier of L;

      synonym Sup F for \\/ (F,L);

      synonym Inf F for //\ (F,L);

    end

    reserve J for non empty set,

j for Element of J;

    theorem :: YELLOW_2:53

    for F be Function of J, the carrier of L holds (F . j) <= ( Sup F) & ( Inf F) <= (F . j)

    proof

      let F be Function of J, the carrier of L;

      (F . j) in ( rng F) by FUNCT_2: 4;

      hence thesis by Th22;

    end;

    theorem :: YELLOW_2:54

    for F be Function of J, the carrier of L holds (for j holds (F . j) <= a) implies ( Sup F) <= a

    proof

      let F be Function of J, the carrier of L;

      assume

       A1: for j holds (F . j) <= a;

      now

        let c be Element of L;

        assume c in ( rng F);

        then

        consider j be object such that

         A2: j in ( dom F) and

         A3: c = (F . j) by FUNCT_1:def 3;

        reconsider j as Element of J by A2;

        c = (F . j) by A3;

        hence c <= a by A1;

      end;

      then ( rng F) is_<=_than a;

      hence thesis by YELLOW_0: 32;

    end;

    theorem :: YELLOW_2:55

    for F be Function of J, the carrier of L holds (for j holds a <= (F . j)) implies a <= ( Inf F)

    proof

      let F be Function of J, the carrier of L;

      assume

       A1: for j holds a <= (F . j);

      now

        let c be Element of L;

        assume c in ( rng F);

        then

        consider j be object such that

         A2: j in ( dom F) and

         A3: c = (F . j) by FUNCT_1:def 3;

        reconsider j as Element of J by A2;

        c = (F . j) by A3;

        hence a <= c by A1;

      end;

      then a is_<=_than ( rng F);

      hence thesis by YELLOW_0: 33;

    end;