lattice5.miz



    begin

    theorem :: LATTICE5:1

    

     Th1: for f be Function, F be Function-yielding Function st f = ( union ( rng F)) holds ( dom f) = ( union ( rng ( doms F)))

    proof

      let f be Function;

      let F be Function-yielding Function;

      assume

       A1: f = ( union ( rng F));

      thus ( dom f) c= ( union ( rng ( doms F)))

      proof

        let x be object;

        assume x in ( dom f);

        then [x, (f . x)] in ( union ( rng F)) by A1, FUNCT_1:def 2;

        then

        consider g be set such that

         A2: [x, (f . x)] in g and

         A3: g in ( rng F) by TARSKI:def 4;

        consider u be object such that

         A4: u in ( dom F) and

         A5: g = (F . u) by A3, FUNCT_1:def 3;

        u in ( dom ( doms F)) by A4, A5, FUNCT_6: 22;

        then

         A6: (( doms F) . u) in ( rng ( doms F)) by FUNCT_1:def 3;

        x in ( dom (F . u)) by A2, A5, FUNCT_1: 1;

        then x in (( doms F) . u) by A4, FUNCT_6: 22;

        hence thesis by A6, TARSKI:def 4;

      end;

      let x be object;

      assume x in ( union ( rng ( doms F)));

      then

      consider A be set such that

       A7: x in A and

       A8: A in ( rng ( doms F)) by TARSKI:def 4;

      consider u be object such that

       A9: u in ( dom ( doms F)) and

       A10: A = (( doms F) . u) by A8, FUNCT_1:def 3;

      

       A11: u in ( dom F) by A9, FUNCT_6: 59;

      then

       A12: (F . u) in ( rng F) by FUNCT_1:def 3;

      consider g be Function such that

       A13: g = (F . u);

      A = ( dom (F . u)) by A10, A11, FUNCT_6: 22;

      then [x, (g . x)] in (F . u) by A7, A13, FUNCT_1:def 2;

      then [x, (g . x)] in f by A1, A12, TARSKI:def 4;

      hence thesis by FUNCT_1: 1;

    end;

    theorem :: LATTICE5:2

    

     Th2: for A,B be non empty set holds [:( union A), ( union B):] = ( union { [:a, b:] where a be Element of A, b be Element of B : a in A & b in B })

    proof

      let A,B be non empty set;

      set Y = { [:a, b:] where a be Element of A, b be Element of B : a in A & b in B };

      thus [:( union A), ( union B):] c= ( union Y)

      proof

        let z be object;

        assume

         A1: z in [:( union A), ( union B):];

        then

        consider x,y be object such that

         A2: z = [x, y] by RELAT_1:def 1;

        y in ( union B) by A1, A2, ZFMISC_1: 87;

        then

        consider b9 be set such that

         A3: y in b9 and

         A4: b9 in B by TARSKI:def 4;

        x in ( union A) by A1, A2, ZFMISC_1: 87;

        then

        consider a9 be set such that

         A5: x in a9 and

         A6: a9 in A by TARSKI:def 4;

        reconsider b9 as Element of B by A4;

        reconsider a9 as Element of A by A6;

        

         A7: [:a9, b9:] in Y;

        z in [:a9, b9:] by A2, A5, A3, ZFMISC_1:def 2;

        hence thesis by A7, TARSKI:def 4;

      end;

      let z be object;

      assume z in ( union Y);

      then

      consider e be set such that

       A8: z in e and

       A9: e in Y by TARSKI:def 4;

      consider a9 be Element of A, b9 be Element of B such that

       A10: [:a9, b9:] = e and a9 in A and b9 in B by A9;

      consider x,y be object such that

       A11: x in a9 & y in b9 and

       A12: z = [x, y] by A8, A10, ZFMISC_1:def 2;

      x in ( union A) & y in ( union B) by A11, TARSKI:def 4;

      hence thesis by A12, ZFMISC_1:def 2;

    end;

    theorem :: LATTICE5:3

    

     Th3: for A be non empty set st A is c=-linear holds [:( union A), ( union A):] = ( union { [:a, a:] where a be Element of A : a in A })

    proof

      let A be non empty set;

      set X = { [:a, a:] where a be Element of A : a in A }, Y = { [:a, b:] where a be Element of A, b be Element of A : a in A & b in A };

      assume

       A1: A is c=-linear;

      

       A2: ( union Y) c= ( union X)

      proof

        let Z be object;

        assume Z in ( union Y);

        then

        consider z be set such that

         A3: Z in z and

         A4: z in Y by TARSKI:def 4;

        consider a,b be Element of A such that

         A5: z = [:a, b:] and a in A and b in A by A4;

        

         A6: (a,b) are_c=-comparable by A1;

        per cases by A6;

          suppose

           A7: a c= b;

          

           A8: [:b, b:] in X;

           [:a, b:] c= [:b, b:] by A7, ZFMISC_1: 95;

          hence thesis by A3, A5, A8, TARSKI:def 4;

        end;

          suppose

           A9: b c= a;

          

           A10: [:a, a:] in X;

           [:a, b:] c= [:a, a:] by A9, ZFMISC_1: 95;

          hence thesis by A3, A5, A10, TARSKI:def 4;

        end;

      end;

      X c= Y

      proof

        let Z be object;

        assume Z in X;

        then ex a be Element of A st Z = [:a, a:] & a in A;

        hence thesis;

      end;

      then ( union X) c= ( union Y) by ZFMISC_1: 77;

      then ( union X) = ( union Y) by A2;

      hence thesis by Th2;

    end;

    begin

    reserve X for non empty set;

    definition

      let A be set;

      :: LATTICE5:def1

      func EqRelLATT A -> Poset equals ( LattPOSet ( EqRelLatt A));

      correctness ;

    end

    registration

      let A be set;

      cluster ( EqRelLATT A) -> with_infima with_suprema;

      coherence ;

    end

    theorem :: LATTICE5:4

    

     Th4: for A,x be set holds x in the carrier of ( EqRelLATT A) iff x is Equivalence_Relation of A

    proof

      let A,x be set;

      hereby

        assume x in the carrier of ( EqRelLATT A);

        then

        reconsider e = x as Element of ( LattPOSet ( EqRelLatt A));

        ( % e) = e;

        then

         A1: x in the carrier of ( EqRelLatt A);

        the carrier of ( EqRelLatt A) = { r where r be Relation of A, A : r is Equivalence_Relation of A } by MSUALG_5:def 2;

        then ex x9 be Relation of A, A st x9 = x & x9 is Equivalence_Relation of A by A1;

        hence x is Equivalence_Relation of A;

      end;

      

       A2: the carrier of ( EqRelLatt A) = { r where r be Relation of A, A : r is Equivalence_Relation of A } by MSUALG_5:def 2;

      assume x is Equivalence_Relation of A;

      then x in the carrier of ( EqRelLatt A) by A2;

      then

      reconsider e = x as Element of ( EqRelLatt A);

      reconsider e as Element of ( EqRelLATT A);

      e in the carrier of ( EqRelLATT A);

      hence thesis;

    end;

    theorem :: LATTICE5:5

    

     Th5: for A be set, x,y be Element of ( EqRelLatt A) holds x [= y iff x c= y

    proof

      let A be set, x,y be Element of ( EqRelLatt A);

      reconsider x9 = x, y9 = y as Equivalence_Relation of A by MSUALG_5: 21;

      

       A1: (x9 /\ y9) = x9 iff x9 c= y9 by XBOOLE_1: 17, XBOOLE_1: 28;

      (x "/\" y) = (the L_meet of ( EqRelLatt A) . (x9,y9)) by LATTICES:def 2

      .= (x9 /\ y9) by MSUALG_5:def 2;

      hence thesis by A1, LATTICES: 4;

    end;

    theorem :: LATTICE5:6

    

     Th6: for A be set, a,b be Element of ( EqRelLATT A) holds a <= b iff a c= b

    proof

      let A be set, a,b be Element of ( EqRelLATT A);

      set El = ( EqRelLatt A);

      reconsider a9 = a as Element of El;

      reconsider b9 = b as Element of El;

      thus a <= b implies a c= b

      proof

        assume a <= b;

        then (a9 % ) <= (b9 % );

        then a9 [= b9 by LATTICE3: 7;

        hence thesis by Th5;

      end;

      thus a c= b implies a <= b

      proof

        assume a c= b;

        then a9 [= b9 by Th5;

        then (a9 % ) <= (b9 % ) by LATTICE3: 7;

        hence thesis;

      end;

    end;

    theorem :: LATTICE5:7

    

     Th7: for L be Lattice, a,b be Element of ( LattPOSet L) holds (a "/\" b) = (( % a) "/\" ( % b))

    proof

      let L be Lattice, a,b be Element of ( LattPOSet L);

      reconsider x = a, y = b as Element of L;

      set c = (x "/\" y);

      

       A1: c [= x by LATTICES: 6;

      

       A2: c [= y by LATTICES: 6;

      

       A3: (c % ) = c;

      reconsider c as Element of ( LattPOSet L);

      

       A4: (y % ) = y;

      then

       A5: c <= b by A2, A3, LATTICE3: 7;

      

       A6: (x % ) = x;

      

       A7: for d be Element of ( LattPOSet L) st d <= a & d <= b holds d <= c

      proof

        let d be Element of ( LattPOSet L);

        reconsider z = d as Element of L;

        

         A8: (z % ) = z;

        assume d <= a & d <= b;

        then z [= x & z [= y by A6, A4, A8, LATTICE3: 7;

        then z [= (x "/\" y) by FILTER_0: 7;

        hence thesis by A3, A8, LATTICE3: 7;

      end;

      c <= a by A1, A3, A6, LATTICE3: 7;

      hence thesis by A5, A7, YELLOW_0: 23;

    end;

    theorem :: LATTICE5:8

    

     Th8: for A be set, a,b be Element of ( EqRelLATT A) holds (a "/\" b) = (a /\ b)

    proof

      let A be set, a,b be Element of ( EqRelLATT A);

       A1:

      now

        let x,y be Element of ( EqRelLatt A);

        reconsider e1 = x as Equivalence_Relation of A by MSUALG_5: 21;

        reconsider e2 = y as Equivalence_Relation of A by MSUALG_5: 21;

        

        thus (x "/\" y) = (the L_meet of ( EqRelLatt A) . (e1,e2)) by LATTICES:def 2

        .= (x /\ y) by MSUALG_5:def 2;

      end;

      reconsider y = b as Element of ( LattPOSet ( EqRelLatt A));

      reconsider x = a as Element of ( LattPOSet ( EqRelLatt A));

      reconsider x as Element of ( EqRelLatt A);

      reconsider y as Element of ( EqRelLatt A);

      ( % (x % )) = (x % ) & ( % (y % )) = (y % );

      

      hence (a "/\" b) = (x "/\" y) by Th7

      .= (a /\ b) by A1;

    end;

    theorem :: LATTICE5:9

    

     Th9: for L be Lattice, a,b be Element of ( LattPOSet L) holds (a "\/" b) = (( % a) "\/" ( % b))

    proof

      let L be Lattice, a,b be Element of ( LattPOSet L);

      reconsider x = a, y = b as Element of L;

      set c = (x "\/" y);

      

       A1: (c % ) = c;

      

       A2: y [= c & (y % ) = y by LATTICES: 5;

      

       A3: x [= c & (x % ) = x by LATTICES: 5;

      reconsider c as Element of ( LattPOSet L);

      

       A4: b <= c by A1, A2, LATTICE3: 7;

      

       A5: for d be Element of ( LattPOSet L) st a <= d & b <= d holds c <= d

      proof

        let d be Element of ( LattPOSet L);

        assume that

         A6: a <= d and

         A7: b <= d;

        reconsider z = d as Element of L;

        (y % ) <= (z % ) by A7;

        then

         A8: y [= z by LATTICE3: 7;

        (x % ) <= (z % ) by A6;

        then x [= z by LATTICE3: 7;

        then (x "\/" y) [= z by A8, FILTER_0: 6;

        then ((x "\/" y) % ) <= (z % ) by LATTICE3: 7;

        hence thesis;

      end;

      a <= c by A1, A3, LATTICE3: 7;

      hence thesis by A4, A5, YELLOW_0: 22;

    end;

    theorem :: LATTICE5:10

    

     Th10: for A be set, a,b be Element of ( EqRelLATT A) holds for E1,E2 be Equivalence_Relation of A st a = E1 & b = E2 holds (a "\/" b) = (E1 "\/" E2)

    proof

      let A be set, a,b be Element of ( EqRelLATT A), E1,E2 be Equivalence_Relation of A;

      assume

       A1: a = E1 & b = E2;

      reconsider y = b as Element of ( LattPOSet ( EqRelLatt A));

      reconsider x = a as Element of ( LattPOSet ( EqRelLatt A));

      reconsider x as Element of ( EqRelLatt A);

      reconsider y as Element of ( EqRelLatt A);

      ( % (x % )) = (x % ) & ( % (y % )) = (y % );

      

      hence (a "\/" b) = (x "\/" y) by Th9

      .= (the L_join of ( EqRelLatt A) . (x,y)) by LATTICES:def 1

      .= (E1 "\/" E2) by A1, MSUALG_5:def 2;

    end;

    definition

      let L be non empty RelStr;

      :: original: complete

      redefine

      :: LATTICE5:def2

      attr L is complete means for X be Subset of L holds ex a be Element of L st a is_<=_than X & for b be Element of L st b is_<=_than X holds b <= a;

      compatibility

      proof

        hereby

          assume

           A1: L is complete;

          let X be Subset of L;

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

          consider p be Element of L such that

           A2: Y is_<=_than p and

           A3: for r be Element of L st Y is_<=_than r holds p <= r by A1;

          take p;

          thus p is_<=_than X

          proof

            let q be Element of L;

            assume

             A4: q in X;

            Y is_<=_than q

            proof

              let s be Element of L;

              assume s in Y;

              then ex t be Element of L st s = t & t is_<=_than X;

              hence thesis by A4;

            end;

            hence thesis by A3;

          end;

          let b be Element of L;

          assume b is_<=_than X;

          then b in Y;

          hence b <= p by A2;

        end;

        assume

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

        let X be set;

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

        Y c= the carrier of L

        proof

          let x be object;

          assume x in Y;

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

          hence thesis;

        end;

        then

        consider p be Element of L such that

         A6: p is_<=_than Y and

         A7: for r be Element of L st r is_<=_than Y holds r <= p by A5;

        take p;

        thus X is_<=_than p

        proof

          let q be Element of L;

          assume

           A8: q in X;

          q is_<=_than Y

          proof

            let s be Element of L;

            assume s in Y;

            then ex t be Element of L st s = t & X is_<=_than t;

            hence thesis by A8;

          end;

          hence thesis by A7;

        end;

        let r be Element of L;

        assume X is_<=_than r;

        then r in Y;

        hence thesis by A6;

      end;

    end

    registration

      let A be set;

      cluster ( EqRelLATT A) -> complete;

      coherence

      proof

        let X be Subset of ( EqRelLATT A);

        set B = (X /\ the carrier of ( EqRelLATT A));

        B c= ( bool [:A, A:])

        proof

          let x be object;

          assume x in B;

          then x is Equivalence_Relation of A by Th4;

          hence thesis;

        end;

        then

        reconsider B as Subset-Family of [:A, A:];

        consider b be Subset of [:A, A:] such that

         A1: b = ( Intersect B);

        for x be object holds x in A implies [x, x] in b

        proof

          let x be object;

          assume

           A2: x in A;

          

           A3: for Y be set st Y in B holds [x, x] in Y

          proof

            let Y be set;

            assume Y in B;

            then Y is Equivalence_Relation of A by Th4;

            hence thesis by A2, EQREL_1: 5;

          end;

           [x, x] in [:A, A:] by A2, ZFMISC_1:def 2;

          hence thesis by A1, A3, SETFAM_1: 43;

        end;

        then

         A4: b is_reflexive_in A by RELAT_2:def 1;

        reconsider b as Relation of A;

        

         A5: ( dom b) = A & ( field b) = A by A4, ORDERS_1: 13;

        for x,y,z be object holds x in A & y in A & z in A & [x, y] in b & [y, z] in b implies [x, z] in b

        proof

          let x,y,z be object;

          assume that

           A6: x in A and y in A and

           A7: z in A and

           A8: [x, y] in b & [y, z] in b;

          

           A9: for Y be set st Y in B holds [x, z] in Y

          proof

            let Y be set;

            assume

             A10: Y in B;

            then

             A11: Y is Equivalence_Relation of A by Th4;

             [x, y] in Y & [y, z] in Y by A1, A8, A10, SETFAM_1: 43;

            hence thesis by A11, EQREL_1: 7;

          end;

           [x, z] in [:A, A:] by A6, A7, ZFMISC_1:def 2;

          hence thesis by A1, A9, SETFAM_1: 43;

        end;

        then

         A12: b is_transitive_in A by RELAT_2:def 8;

        for x,y be object st x in A & y in A & [x, y] in b holds [y, x] in b

        proof

          let x,y be object;

          assume that

           A13: x in A & y in A and

           A14: [x, y] in b;

          

           A15: for Y be set st Y in B holds [y, x] in Y

          proof

            let Y be set;

            assume Y in B;

            then [x, y] in Y & Y is Equivalence_Relation of A by A1, A14, Th4, SETFAM_1: 43;

            hence thesis by EQREL_1: 6;

          end;

           [y, x] in [:A, A:] by A13, ZFMISC_1:def 2;

          hence thesis by A1, A15, SETFAM_1: 43;

        end;

        then b is_symmetric_in A by RELAT_2:def 3;

        then

        reconsider b as Equivalence_Relation of A by A5, A12, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16;

        reconsider b as Element of ( EqRelLATT A) by Th4;

        take b;

        now

          let a be Element of ( EqRelLATT A);

          reconsider a9 = a as Equivalence_Relation of A by Th4;

          reconsider b9 = b as Equivalence_Relation of A;

          assume a in (X /\ the carrier of ( EqRelLATT A));

          then for x,y be object holds [x, y] in b9 implies [x, y] in a9 by A1, SETFAM_1: 43;

          then b9 c= a9 by RELAT_1:def 3;

          hence b <= a by Th6;

        end;

        then b is_<=_than (X /\ the carrier of ( EqRelLATT A));

        hence b is_<=_than X by YELLOW_0: 5;

        let a be Element of ( EqRelLATT A);

        reconsider a9 = a as Equivalence_Relation of A by Th4;

        assume a is_<=_than X;

        then

         A16: a is_<=_than (X /\ the carrier of ( EqRelLATT A)) by YELLOW_0: 5;

        

         A17: for d be Element of ( EqRelLATT A) st d in B holds a9 c= d by A16, Th6;

        a9 c= ( Intersect B)

        proof

          let x be object;

          assume

           A18: x in a9;

          for Y be set st Y in B holds x in Y

          proof

            let Y be set;

            assume Y in B;

            then a9 c= Y by A17;

            hence thesis by A18;

          end;

          hence thesis by A18, SETFAM_1: 43;

        end;

        hence a <= b by A1, Th6;

      end;

    end

    begin

    registration

      let L1,L2 be LATTICE;

      cluster meet-preserving join-preserving for Function of L1, L2;

      existence

      proof

        set z = the Element of L2;

        reconsider f = (the carrier of L1 --> z) as Function of L1, L2;

        take f;

        for x,y be Element of L1 holds (f . (x "/\" y)) = ((f . x) "/\" (f . y)) by YELLOW_5: 2;

        hence f is meet-preserving by WAYBEL_6: 1;

        for x,y be Element of L1 holds (f . (x "\/" y)) = ((f . x) "\/" (f . y)) by YELLOW_5: 1;

        hence thesis by WAYBEL_6: 2;

      end;

    end

    definition

      let L1,L2 be LATTICE;

      mode Homomorphism of L1,L2 is meet-preserving join-preserving Function of L1, L2;

    end

    registration

      let L be LATTICE;

      cluster meet-inheriting join-inheriting strict for SubRelStr of L;

      existence

      proof

        set a = the Element of L;

        set r = the Relation of {a};

        

         A1: for x,y be Element of L st x in {a} & y in {a} & ex_sup_of ( {x, y},L) holds ( sup {x, y}) in {a}

        proof

          let x,y be Element of L;

          assume that

           A2: x in {a} & y in {a} and ex_sup_of ( {x, y},L);

          x = a & y = a by A2, TARSKI:def 1;

          

          then ( sup {x, y}) = (a "\/" a) by YELLOW_0: 41

          .= a by YELLOW_5: 1;

          hence thesis by TARSKI:def 1;

        end;

        r c= the InternalRel of L

        proof

          let z be object;

          assume z in r;

          then

          consider x,y be object such that

           A3: z = [x, y] and

           A4: x in {a} and

           A5: y in {a} by RELSET_1: 2;

          x = a by A4, TARSKI:def 1;

          then

           A6: z = [a, a] by A3, A5, TARSKI:def 1;

          a <= a;

          hence thesis by A6, ORDERS_2:def 5;

        end;

        then

        reconsider S = RelStr (# {a}, r #) as strict SubRelStr of L by YELLOW_0:def 13;

        take S;

        for x,y be Element of L st x in {a} & y in {a} & ex_inf_of ( {x, y},L) holds ( inf {x, y}) in {a}

        proof

          let x,y be Element of L;

          assume that

           A7: x in {a} & y in {a} and ex_inf_of ( {x, y},L);

          x = a & y = a by A7, TARSKI:def 1;

          

          then ( inf {x, y}) = (a "/\" a) by YELLOW_0: 40

          .= a by YELLOW_5: 2;

          hence thesis by TARSKI:def 1;

        end;

        hence thesis by A1, YELLOW_0:def 16, YELLOW_0:def 17;

      end;

    end

    definition

      let L be non empty RelStr;

      mode Sublattice of L is meet-inheriting join-inheriting SubRelStr of L;

    end

    registration

      let L1,L2 be LATTICE;

      let f be Homomorphism of L1, L2;

      cluster ( Image f) -> meet-inheriting join-inheriting;

      coherence

      proof

        set S = ( subrelstr ( rng f));

        

         A1: the carrier of S = ( rng f) by YELLOW_0:def 15;

        

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

        for x,y be Element of L2 st x in the carrier of S & y in the carrier of S & ex_sup_of ( {x, y},L2) holds ( sup {x, y}) in the carrier of S

        proof

          let x,y be Element of L2;

          assume that

           A3: x in the carrier of S and

           A4: y in the carrier of S and ex_sup_of ( {x, y},L2);

          consider a be object such that

           A5: a in ( dom f) and

           A6: x = (f . a) by A1, A3, FUNCT_1:def 3;

          consider b be object such that

           A7: b in ( dom f) and

           A8: y = (f . b) by A1, A4, FUNCT_1:def 3;

          reconsider a9 = a, b9 = b as Element of L1 by A5, A7;

          

           A9: f preserves_sup_of {a9, b9} & ex_sup_of ( {a9, b9},L1) by WAYBEL_0:def 35, YELLOW_0: 20;

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

          .= (f . ( sup {a9, b9})) by A9;

          hence thesis by A1, A2, FUNCT_1:def 3;

        end;

        then

         A10: S is join-inheriting by YELLOW_0:def 17;

        for x,y be Element of L2 st x in the carrier of S & y in the carrier of S & ex_inf_of ( {x, y},L2) holds ( inf {x, y}) in the carrier of S

        proof

          let x,y be Element of L2;

          assume that

           A11: x in the carrier of S and

           A12: y in the carrier of S and ex_inf_of ( {x, y},L2);

          consider a be object such that

           A13: a in ( dom f) and

           A14: x = (f . a) by A1, A11, FUNCT_1:def 3;

          consider b be object such that

           A15: b in ( dom f) and

           A16: y = (f . b) by A1, A12, FUNCT_1:def 3;

          reconsider a9 = a, b9 = b as Element of L1 by A13, A15;

          

           A17: f preserves_inf_of {a9, b9} & ex_inf_of ( {a9, b9},L1) by WAYBEL_0:def 34, YELLOW_0: 21;

          ( inf {x, y}) = ( inf (f .: {a9, b9})) by A13, A14, A15, A16, FUNCT_1: 60

          .= (f . ( inf {a9, b9})) by A17;

          hence thesis by A1, A2, FUNCT_1:def 3;

        end;

        then S is meet-inheriting by YELLOW_0:def 16;

        hence thesis by A10, YELLOW_2:def 2;

      end;

    end

    reserve e,e1,e2,e19,e29 for Equivalence_Relation of X,

x,y,x9,y9 for set;

    definition

      let X;

      let f be non empty FinSequence of X;

      let x,y be object;

      let R1,R2 be Relation;

      :: LATTICE5:def3

      pred x,y are_joint_by f,R1,R2 means (f . 1) = x & (f . ( len f)) = y & for i be Element of NAT st 1 <= i & i < ( len f) holds (i is odd implies [(f . i), (f . (i + 1))] in R1) & (i is even implies [(f . i), (f . (i + 1))] in R2);

    end

    theorem :: LATTICE5:11

    

     Th11: for x be set, o be Element of NAT , R1,R2 be Relation, f be non empty FinSequence of X st R1 is_reflexive_in X & R2 is_reflexive_in X & f = (o |-> x) holds (x,x) are_joint_by (f,R1,R2)

    proof

      let x be set, o be Element of NAT , R1,R2 be Relation, f be non empty FinSequence of X;

      assume that

       A1: R1 is_reflexive_in X and

       A2: R2 is_reflexive_in X and

       A3: f = (o |-> x);

      

       A4: ( dom f) = ( Seg o) by A3;

      then

       A5: (f . 1) = x by A3, FINSEQ_5: 6, FUNCOP_1: 7;

      

       A6: for i be Element of NAT st 1 <= i & i < ( len f) holds (i is odd implies [(f . i), (f . (i + 1))] in R1) & (i is even implies [(f . i), (f . (i + 1))] in R2)

      proof

        let i be Element of NAT ;

        assume that

         A7: 1 <= i and

         A8: i < ( len f);

        

         A9: i is even implies [(f . i), (f . (i + 1))] in R2

        proof

          1 <= (i + 1) & (i + 1) <= ( len f) by A7, A8, NAT_1: 13;

          then (i + 1) in ( Seg ( len f));

          then (i + 1) in ( Seg o) by A3, CARD_1:def 7;

          then

           A10: (f . (i + 1)) = x by A3, FUNCOP_1: 7;

          assume i is even;

          i <= o by A3, A8, CARD_1:def 7;

          then i in ( Seg o) by A7;

          then

           A11: (f . i) = x by A3, FUNCOP_1: 7;

          x in X by A4, A5, FINSEQ_2: 11, FINSEQ_5: 6;

          hence thesis by A2, A10, A11, RELAT_2:def 1;

        end;

        i is odd implies [(f . i), (f . (i + 1))] in R1

        proof

          1 <= (i + 1) & (i + 1) <= ( len f) by A7, A8, NAT_1: 13;

          then (i + 1) in ( Seg ( len f));

          then (i + 1) in ( Seg o) by A3, CARD_1:def 7;

          then

           A12: (f . (i + 1)) = x by A3, FUNCOP_1: 7;

          assume i is odd;

          i <= o by A3, A8, CARD_1:def 7;

          then i in ( Seg o) by A7;

          then

           A13: (f . i) = x by A3, FUNCOP_1: 7;

          x in X by A4, A5, FINSEQ_2: 11, FINSEQ_5: 6;

          hence thesis by A1, A12, A13, RELAT_2:def 1;

        end;

        hence thesis by A9;

      end;

      ( len f) in ( Seg o) by A4, FINSEQ_5: 6;

      then (f . ( len f)) = x by A3, FUNCOP_1: 7;

      hence thesis by A5, A6;

    end;

     Lm1:

    now

      let i,n,m be Element of NAT ;

      assume 1 <= i & i < (n + m);

      then 1 <= i & i < n or n = i & i < (n + m) or n < i & i < (n + m) by XXREAL_0: 1;

      hence 1 <= i & i < n or n = i & i < (n + m) or (n + 1) <= i & i < (n + m) by NAT_1: 13;

    end;

    theorem :: LATTICE5:12

    

     Th12: for x,y be object, R1,R2 be Relation, n,m be Element of NAT st (n <= m & R1 is_reflexive_in X & R2 is_reflexive_in X & ex f be non empty FinSequence of X st ( len f) = n & (x,y) are_joint_by (f,R1,R2)) holds ex h be non empty FinSequence of X st ( len h) = m & (x,y) are_joint_by (h,R1,R2)

    proof

      let x,y be object, R1,R2 be Relation, n,m be Element of NAT ;

      assume that

       A1: n <= m and

       A2: R1 is_reflexive_in X and

       A3: R2 is_reflexive_in X;

      given f be non empty FinSequence of X such that

       A4: ( len f) = n and

       A5: (x,y) are_joint_by (f,R1,R2);

      

       A6: (f . ( len f)) = y by A5;

      per cases by A1, XXREAL_0: 1;

        suppose

         A7: n < m;

        ( len f) in ( dom f) by FINSEQ_5: 6;

        then y in ( rng f) by A6, FUNCT_1:def 3;

        then

        reconsider y9 = y as Element of X;

        reconsider i = (m - n) as Element of NAT by A1, INT_1: 5;

        reconsider g = (i |-> y9) as FinSequence of X;

        i > 0 by A7, XREAL_1: 50;

        then

        reconsider g as non empty FinSequence of X;

        

         A8: 1 in ( dom g) by FINSEQ_5: 6;

        reconsider h = (f ^ g) as non empty FinSequence of X;

        take h;

        

         A9: ( len g) = (m - n) by CARD_1:def 7;

        

         A10: (y,y) are_joint_by (g,R1,R2) by A2, A3, Th11;

        

        thus ( len h) = (( len f) + ( len g)) by FINSEQ_1: 22

        .= (n + (m - n)) by A4, CARD_1:def 7

        .= m;

        

         A11: ( len g) in ( dom g) by FINSEQ_5: 6;

        thus (x,y) are_joint_by (h,R1,R2)

        proof

          ( rng f) <> {} ;

          then 1 in ( dom f) by FINSEQ_3: 32;

          

          hence (h . 1) = (f . 1) by FINSEQ_1:def 7

          .= x by A5;

          

          thus (h . ( len h)) = (h . (( len f) + ( len g))) by FINSEQ_1: 22

          .= (g . ( len g)) by A11, FINSEQ_1:def 7

          .= y by A10;

          let j be Element of NAT ;

          

           A12: ( dom f) = ( Seg ( len f)) by FINSEQ_1:def 3;

          assume

           A13: 1 <= j & j < ( len h);

          thus j is odd implies [(h . j), (h . (j + 1))] in R1

          proof

            assume

             A14: j is odd;

            per cases by A13, Lm1, FINSEQ_1: 22;

              suppose

               A15: 1 <= j & j < ( len f);

              then 1 <= (j + 1) & (j + 1) <= ( len f) by NAT_1: 13;

              then (j + 1) in ( dom f) by A12;

              then

               A16: (f . (j + 1)) = (h . (j + 1)) by FINSEQ_1:def 7;

              j in ( dom f) by A12, A15;

              then (f . j) = (h . j) by FINSEQ_1:def 7;

              hence thesis by A5, A14, A15, A16;

            end;

              suppose

               A17: j = ( len f);

              then j in ( dom f) by FINSEQ_5: 6;

              then

               A18: (h . j) = y by A6, A17, FINSEQ_1:def 7;

              (h . (j + 1)) = (g . 1) by A8, A17, FINSEQ_1:def 7

              .= y by A10;

              hence thesis by A2, A18, RELAT_2:def 1;

            end;

              suppose

               A19: (( len f) + 1) <= j & j < (( len f) + ( len g));

              then (j + 1) <= (( len f) + ( len g)) by NAT_1: 13;

              then

               A20: (j + 1) <= ( len h) by FINSEQ_1: 22;

              

               A21: 1 <= (j - ( len f)) by A19, XREAL_1: 19;

              then 0 < (j - ( len f)) by XXREAL_0: 2;

              then

               A22: ( 0 + ( len f)) < ((j - ( len f)) + ( len f)) by XREAL_1: 6;

              then

              reconsider k = (j - ( len f)) as Element of NAT by INT_1: 5;

              

               A23: (j - ( len f)) < ((( len f) + ( len g)) - ( len f)) by A19, XREAL_1: 9;

              then

               A24: (k + 1) <= ( len g) by NAT_1: 13;

              j < (j + 1) by XREAL_1: 29;

              then ( len f) < (j + 1) by A22, XXREAL_0: 2;

              

              then

               A25: (h . (j + 1)) = (g . ((j + 1) - ( len f))) by A20, FINSEQ_1: 24

              .= (g . (k + 1));

              1 <= (k + 1) by A21, NAT_1: 13;

              then (k + 1) in ( Seg ( len g)) by A24;

              then

               A26: (g . (k + 1)) = y by A9, FUNCOP_1: 7;

              k in ( Seg ( len g)) by A21, A23;

              then (g . k) = y by A9, FUNCOP_1: 7;

              then (h . j) = y by A19, FINSEQ_1: 23;

              hence thesis by A2, A26, A25, RELAT_2:def 1;

            end;

          end;

          assume

           A27: j is even;

          per cases by A13, Lm1, FINSEQ_1: 22;

            suppose

             A28: 1 <= j & j < ( len f);

            then 1 <= (j + 1) & (j + 1) <= ( len f) by NAT_1: 13;

            then (j + 1) in ( dom f) by A12;

            then

             A29: (f . (j + 1)) = (h . (j + 1)) by FINSEQ_1:def 7;

            j in ( dom f) by A12, A28;

            then (f . j) = (h . j) by FINSEQ_1:def 7;

            hence thesis by A5, A27, A28, A29;

          end;

            suppose

             A30: j = ( len f);

            then j in ( dom f) by FINSEQ_5: 6;

            then

             A31: (h . j) = y by A6, A30, FINSEQ_1:def 7;

            (h . (j + 1)) = (g . 1) by A8, A30, FINSEQ_1:def 7

            .= y by A10;

            hence thesis by A3, A31, RELAT_2:def 1;

          end;

            suppose

             A32: (( len f) + 1) <= j & j < (( len f) + ( len g));

            then (j + 1) <= (( len f) + ( len g)) by NAT_1: 13;

            then

             A33: (j + 1) <= ( len h) by FINSEQ_1: 22;

            

             A34: 1 <= (j - ( len f)) by A32, XREAL_1: 19;

            then 0 < (j - ( len f)) by XXREAL_0: 2;

            then

             A35: ( 0 + ( len f)) < ((j - ( len f)) + ( len f)) by XREAL_1: 6;

            then

            reconsider k = (j - ( len f)) as Element of NAT by INT_1: 5;

            

             A36: (j - ( len f)) < ((( len f) + ( len g)) - ( len f)) by A32, XREAL_1: 9;

            then

             A37: (k + 1) <= ( len g) by NAT_1: 13;

            j < (j + 1) by XREAL_1: 29;

            then ( len f) < (j + 1) by A35, XXREAL_0: 2;

            

            then

             A38: (h . (j + 1)) = (g . ((j + 1) - ( len f))) by A33, FINSEQ_1: 24

            .= (g . (k + 1));

            1 <= (k + 1) by A34, NAT_1: 13;

            then (k + 1) in ( Seg ( len g)) by A37;

            then

             A39: (g . (k + 1)) = y by A9, FUNCOP_1: 7;

            k in ( Seg ( len g)) by A34, A36;

            then (g . k) = y by A9, FUNCOP_1: 7;

            then (h . j) = y by A32, FINSEQ_1: 23;

            hence thesis by A3, A39, A38, RELAT_2:def 1;

          end;

        end;

      end;

        suppose n = m;

        hence thesis by A4, A5;

      end;

    end;

    definition

      let X;

      let Y be Sublattice of ( EqRelLATT X);

      given e such that

       A1: e in the carrier of Y and

       A2: e <> ( id X);

      given o be Element of NAT such that

       A3: for e1, e2 holds for x,y be object st e1 in the carrier of Y & e2 in the carrier of Y & [x, y] in (e1 "\/" e2) holds ex F be non empty FinSequence of X st ( len F) = o & (x,y) are_joint_by (F,e1,e2);

      :: LATTICE5:def4

      func type_of Y -> Element of NAT means

      : Def4: (for e1, e2 holds for x,y be object st e1 in the carrier of Y & e2 in the carrier of Y & [x, y] in (e1 "\/" e2) holds (ex F be non empty FinSequence of X st ( len F) = (it + 2) & (x,y) are_joint_by (F,e1,e2))) & ex e1, e2 st ex x,y be object st e1 in the carrier of Y & e2 in the carrier of Y & [x, y] in (e1 "\/" e2) & not (ex F be non empty FinSequence of X st ( len F) = (it + 1) & (x,y) are_joint_by (F,e1,e2));

      existence

      proof

        defpred X[ Element of NAT ] means for e1, e2 holds for x,y be object st e1 in the carrier of Y & e2 in the carrier of Y & [x, y] in (e1 "\/" e2) holds ex F be non empty FinSequence of X st ( len F) = ($1 + 2) & (x,y) are_joint_by (F,e1,e2);

        set A = { n where n be Element of NAT : X[n] };

        consider e1, e2 such that

         A4: e1 = e & e2 = e;

        

         A5: ( field e) = X by EQREL_1: 9;

        then ( id X) c= e by RELAT_2: 1;

        then not e c= ( id X) by A2;

        then

        consider x,y be object such that

         A6: [x, y] in e and

         A7: not [x, y] in ( id X) by RELAT_1:def 3;

        

         A8: not x in X or x <> y by A7, RELAT_1:def 10;

        

         A9: [x, y] in (e1 "\/" e2) by A6, A4;

        then

        consider F be non empty FinSequence of X such that

         A10: ( len F) = o and

         A11: (x,y) are_joint_by (F,e1,e2) by A1, A3, A4;

        

         A12: (F . 1) = x & (F . ( len F)) = y by A11;

        o >= 2

        proof

          assume not thesis;

          then ( len F) < (1 + 1) by A10;

          then 0 <= ( len F) & ( len F) <= ( 0 + 1) by NAT_1: 2, NAT_1: 13;

          hence contradiction by A5, A6, A8, A12, NAT_1: 9, RELAT_1: 15;

        end;

        then

        consider o9 be Nat such that

         A13: o = (2 + o9) by NAT_1: 10;

        

         A14: A is Subset of NAT from DOMAIN_1:sch 7;

        o9 in NAT by ORDINAL1:def 12;

        then

        consider k be Element of NAT such that k = o9 and

         A15: for e1, e2 holds for x,y be object st e1 in the carrier of Y & e2 in the carrier of Y & [x, y] in (e1 "\/" e2) holds ex F be non empty FinSequence of X st ( len F) = (k + 2) & (x,y) are_joint_by (F,e1,e2) by A3, A13;

        k in A by A15;

        then

        reconsider A as non empty Subset of NAT by A14;

        set m = ( min A);

        

         A16: ex e1, e2 st ex x,y be object st e1 in the carrier of Y & e2 in the carrier of Y & [x, y] in (e1 "\/" e2) & not (ex F be non empty FinSequence of X st ( len F) = (m + 1) & (x,y) are_joint_by (F,e1,e2))

        proof

          assume

           A17: not thesis;

          then

          consider F be non empty FinSequence of X such that

           A18: ( len F) = (m + 1) and

           A19: (x,y) are_joint_by (F,e1,e2) by A1, A4, A9;

          

           A20: (F . 1) = x & (F . ( len F)) = y by A19;

          ( len F) >= 2

          proof

            assume not thesis;

            then ( len F) < (1 + 1);

            then 0 <= ( len F) & ( len F) <= ( 0 + 1) by NAT_1: 2, NAT_1: 13;

            hence contradiction by A5, A6, A8, A20, NAT_1: 9, RELAT_1: 15;

          end;

          then (m + 1) >= (1 + 1) by A18;

          then

           A21: m >= 1 by XREAL_1: 6;

          then (m + 1) = ((m - 1) + 2) & (m - 1) = (m -' 1) by XREAL_1: 233;

          then

           A22: (m -' 1) in A by A17;

          m < (m + 1) by XREAL_1: 29;

          then

           A23: (m - 1) < ((m + 1) - 1) by XREAL_1: 9;

          (m - 1) >= 0 by A21, XREAL_1: 48;

          then (m -' 1) < m by A23, XREAL_0:def 2;

          hence contradiction by A22, XXREAL_2:def 7;

        end;

        m in A by XXREAL_2:def 7;

        then ex m9 be Element of NAT st m9 = m & for e1, e2 holds for x,y be object st e1 in the carrier of Y & e2 in the carrier of Y & [x, y] in (e1 "\/" e2) holds ex F be non empty FinSequence of X st ( len F) = (m9 + 2) & (x,y) are_joint_by (F,e1,e2);

        hence thesis by A16;

      end;

      uniqueness

      proof

        let n1,n2 be Element of NAT ;

        assume

         A24: for e1, e2 holds for x,y be object st e1 in the carrier of Y & e2 in the carrier of Y & [x, y] in (e1 "\/" e2) holds ex F be non empty FinSequence of X st ( len F) = (n1 + 2) & (x,y) are_joint_by (F,e1,e2);

        given e19,e29 be Equivalence_Relation of X, x9,y9 be object such that

         A25: e19 in the carrier of Y & e29 in the carrier of Y & [x9, y9] in (e19 "\/" e29) and

         A26: not (ex F be non empty FinSequence of X st ( len F) = (n1 + 1) & (x9,y9) are_joint_by (F,e19,e29));

        assume for e1, e2 holds for x,y be object st e1 in the carrier of Y & e2 in the carrier of Y & [x, y] in (e1 "\/" e2) holds ex F be non empty FinSequence of X st ( len F) = (n2 + 2) & (x,y) are_joint_by (F,e1,e2);

        then

         A27: ex F2 be non empty FinSequence of X st ( len F2) = (n2 + 2) & (x9,y9) are_joint_by (F2,e19,e29) by A25;

        ( field e29) = X by EQREL_1: 9;

        then

         A28: e29 is_reflexive_in X by RELAT_2:def 9;

        ( field e19) = X by EQREL_1: 9;

        then

         A29: e19 is_reflexive_in X by RELAT_2:def 9;

        given e1,e2 be Equivalence_Relation of X, x,y be object such that

         A30: e1 in the carrier of Y & e2 in the carrier of Y & [x, y] in (e1 "\/" e2) and

         A31: not (ex F be non empty FinSequence of X st ( len F) = (n2 + 1) & (x,y) are_joint_by (F,e1,e2));

        

         A32: ex F1 be non empty FinSequence of X st ( len F1) = (n1 + 2) & (x,y) are_joint_by (F1,e1,e2) by A24, A30;

        ( field e2) = X by EQREL_1: 9;

        then

         A33: e2 is_reflexive_in X by RELAT_2:def 9;

        ( field e1) = X by EQREL_1: 9;

        then

         A34: e1 is_reflexive_in X by RELAT_2:def 9;

        assume

         A35: not thesis;

        per cases by A35, XXREAL_0: 1;

          suppose n1 < n2;

          then (n1 + 2) < (n2 + (1 + 1)) by XREAL_1: 6;

          then (n1 + 2) < ((n2 + 1) + 1);

          then (n1 + 2) <= (n2 + 1) by NAT_1: 13;

          hence contradiction by A31, A32, A34, A33, Th12;

        end;

          suppose n2 < n1;

          then (n2 + 2) < (n1 + (1 + 1)) by XREAL_1: 6;

          then (n2 + 2) < ((n1 + 1) + 1);

          then (n2 + 2) <= (n1 + 1) by NAT_1: 13;

          hence contradiction by A26, A27, A29, A28, Th12;

        end;

      end;

    end

    theorem :: LATTICE5:13

    

     Th13: for Y be Sublattice of ( EqRelLATT X), n be Element of NAT st (ex e st e in the carrier of Y & e <> ( id X)) & (for e1, e2 holds for x,y be object st e1 in the carrier of Y & e2 in the carrier of Y & [x, y] in (e1 "\/" e2) holds (ex F be non empty FinSequence of X st ( len F) = (n + 2) & (x,y) are_joint_by (F,e1,e2))) holds ( type_of Y) <= n

    proof

      let Y be Sublattice of ( EqRelLATT X), n be Element of NAT ;

      assume that

       A1: ex e st e in the carrier of Y & e <> ( id X) and

       A2: for e1, e2 holds for x,y be object st e1 in the carrier of Y & e2 in the carrier of Y & [x, y] in (e1 "\/" e2) holds ex F be non empty FinSequence of X st ( len F) = (n + 2) & (x,y) are_joint_by (F,e1,e2) and

       A3: n < ( type_of Y);

      (n + 1) <= ( type_of Y) by A3, NAT_1: 13;

      then

      consider m be Nat such that

       A4: ( type_of Y) = ((n + 1) + m) by NAT_1: 10;

      reconsider m as Element of NAT by ORDINAL1:def 12;

      (((n + 1) + m) + 1) = ((n + m) + 2);

      then

      consider e1,e2 be Equivalence_Relation of X, x,y be object such that

       A5: e1 in the carrier of Y & e2 in the carrier of Y & [x, y] in (e1 "\/" e2) and

       A6: not (ex F be non empty FinSequence of X st ( len F) = ((n + m) + 2) & (x,y) are_joint_by (F,e1,e2)) by A1, A4, Def4;

      

       A7: ((n + 2) + m) = ((n + m) + 2);

      ( field e2) = X by EQREL_1: 9;

      then

       A8: e2 is_reflexive_in X by RELAT_2:def 9;

      ( field e1) = X by EQREL_1: 9;

      then

       A9: e1 is_reflexive_in X by RELAT_2:def 9;

      ex F1 be non empty FinSequence of X st ( len F1) = (n + 2) & (x,y) are_joint_by (F1,e1,e2) by A2, A5;

      hence contradiction by A6, A9, A8, A7, Th12, NAT_1: 11;

    end;

    begin

    reserve A for non empty set,

L for lower-bounded LATTICE;

    definition

      let A be set, L be 1-sorted;

      mode BiFunction of A,L is Function of [:A, A:], the carrier of L;

    end

    definition

      let A be non empty set, L be 1-sorted;

      let f be BiFunction of A, L;

      let x,y be Element of A;

      :: original: .

      redefine

      func f . (x,y) -> Element of L ;

      coherence

      proof

        reconsider xy = [x, y] as Element of [:A, A:];

        (f . xy) is Element of L;

        hence thesis;

      end;

    end

    definition

      let A;

      let L be 1-sorted;

      let f be BiFunction of A, L;

      :: LATTICE5:def5

      attr f is symmetric means

      : Def5: for x,y be Element of A holds (f . (x,y)) = (f . (y,x));

    end

    definition

      let A, L;

      let f be BiFunction of A, L;

      :: LATTICE5:def6

      attr f is zeroed means

      : Def6: for x be Element of A holds (f . (x,x)) = ( Bottom L);

      :: LATTICE5:def7

      attr f is u.t.i. means

      : Def7: for x,y,z be Element of A holds ((f . (x,y)) "\/" (f . (y,z))) >= (f . (x,z));

    end

    registration

      let A, L;

      cluster symmetric zeroed u.t.i. for BiFunction of A, L;

      existence

      proof

        reconsider f = ( [:A, A:] --> ( Bottom L)) as Function of [:A, A:], the carrier of L;

        

         A1: for x,y be Element of A holds (f . [x, y]) = ( Bottom L);

        reconsider f as BiFunction of A, L;

        for x,y be Element of A holds (f . (x,y)) = (f . (y,x))

        proof

          let x,y be Element of A;

          

          thus (f . (x,y)) = ( Bottom L) by A1

          .= (f . (y,x)) by A1;

        end;

        then

         A2: f is symmetric;

        for x,y,z be Element of A holds ((f . (x,y)) "\/" (f . (y,z))) >= (f . (x,z))

        proof

          let x,y,z be Element of A;

          

           A3: (f . (x,z)) <= ( Bottom L) by A1;

          (f . (x,y)) = ( Bottom L) & (f . (y,z)) = ( Bottom L) by A1;

          hence thesis by A3, YELLOW_5: 1;

        end;

        then

         A4: f is u.t.i.;

        for x be Element of A holds (f . (x,x)) = ( Bottom L) by A1;

        then f is zeroed;

        hence thesis by A2, A4;

      end;

    end

    definition

      let A, L;

      mode distance_function of A,L is symmetric zeroed u.t.i. BiFunction of A, L;

    end

    definition

      let A, L;

      let d be distance_function of A, L;

      :: LATTICE5:def8

      func alpha d -> Function of L, ( EqRelLATT A) means

      : Def8: for e be Element of L holds ex E be Equivalence_Relation of A st E = (it . e) & for x,y be Element of A holds [x, y] in E iff (d . (x,y)) <= e;

      existence

      proof

        defpred X[ Element of L, Element of ( EqRelLATT A)] means ex E be Equivalence_Relation of A st E = $2 & for x,y be Element of A holds [x, y] in E iff (d . (x,y)) <= $1;

        

         A1: for e be Element of L holds ex r be Element of ( EqRelLATT A) st X[e, r]

        proof

          let e be Element of L;

          defpred X[ Element of A, Element of A] means (d . ($1,$2)) <= e;

          consider E be Relation of A, A such that

           A2: for x,y be Element of A holds [x, y] in E iff X[x, y] from RELSET_1:sch 2;

          for x,y be object holds x in A & y in A & [x, y] in E implies [y, x] in E

          proof

            let x,y be object;

            assume that

             A3: x in A and

             A4: y in A and

             A5: [x, y] in E;

            reconsider y9 = y as Element of A by A4;

            reconsider x9 = x as Element of A by A3;

            (d . (x9,y9)) <= e by A2, A5;

            then (d . (y9,x9)) <= e by Def5;

            hence thesis by A2;

          end;

          then

           A6: E is_symmetric_in A by RELAT_2:def 3;

          for x be object holds x in A implies [x, x] in E

          proof

            let x be object;

            assume x in A;

            then

            reconsider x9 = x as Element of A;

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

            then (d . (x9,x9)) <= e by Def6;

            hence thesis by A2;

          end;

          then E is_reflexive_in A by RELAT_2:def 1;

          then

           A7: ( dom E) = A & ( field E) = A by ORDERS_1: 13;

          for x,y,z be object holds x in A & y in A & z in A & [x, y] in E & [y, z] in E implies [x, z] in E

          proof

            let x,y,z be object;

            assume that

             A8: x in A & y in A & z in A and

             A9: [x, y] in E & [y, z] in E;

            reconsider x9 = x, y9 = y, z9 = z as Element of A by A8;

            (d . (x9,y9)) <= e & (d . (y9,z9)) <= e by A2, A9;

            then

             A10: ((d . (x9,y9)) "\/" (d . (y9,z9))) <= e by YELLOW_0: 22;

            (d . (x9,z9)) <= ((d . (x9,y9)) "\/" (d . (y9,z9))) by Def7;

            then (d . (x9,z9)) <= e by A10, ORDERS_2: 3;

            hence thesis by A2;

          end;

          then E is_transitive_in A by RELAT_2:def 8;

          then

          reconsider E as Equivalence_Relation of A by A7, A6, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16;

          reconsider E as Element of ( EqRelLATT A) by Th4;

          ex r be Element of ( EqRelLATT A) st r = E;

          hence thesis by A2;

        end;

        ex f be Function of L, ( EqRelLATT A) st for e be Element of L holds X[e, (f . e)] from FUNCT_2:sch 3( A1);

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function of L, ( EqRelLATT A) such that

         A11: for e be Element of L holds ex E be Equivalence_Relation of A st E = (f1 . e) & for x,y be Element of A holds [x, y] in E iff (d . (x,y)) <= e and

         A12: for e be Element of L holds ex E be Equivalence_Relation of A st E = (f2 . e) & for x,y be Element of A holds [x, y] in E iff (d . (x,y)) <= e;

        reconsider f19 = f1, f29 = f2 as Function of the carrier of L, the carrier of ( EqRelLATT A);

        for e be Element of L holds (f1 . e) = (f2 . e)

        proof

          let e be Element of L;

          consider E1 be Equivalence_Relation of A such that

           A13: E1 = (f1 . e) and

           A14: for x,y be Element of A holds [x, y] in E1 iff (d . (x,y)) <= e by A11;

          consider E2 be Equivalence_Relation of A such that

           A15: E2 = (f2 . e) and

           A16: for x,y be Element of A holds [x, y] in E2 iff (d . (x,y)) <= e by A12;

          

           A17: for x,y be Element of A holds [x, y] in E1 iff [x, y] in E2

          proof

            let x,y be Element of A;

             [x, y] in E1 iff (d . (x,y)) <= e by A14;

            hence thesis by A16;

          end;

          for x,y be object holds [x, y] in E1 iff [x, y] in E2

          proof

            let x,y be object;

            

             A18: ( field E1) = A by EQREL_1: 9;

            hereby

              assume

               A19: [x, y] in E1;

              then

              reconsider x9 = x, y9 = y as Element of A by A18, RELAT_1: 15;

               [x9, y9] in E2 by A17, A19;

              hence [x, y] in E2;

            end;

            assume

             A20: [x, y] in E2;

            ( field E2) = A by EQREL_1: 9;

            then

            reconsider x9 = x, y9 = y as Element of A by A20, RELAT_1: 15;

             [x9, y9] in E1 by A17, A20;

            hence thesis;

          end;

          hence thesis by A13, A15, RELAT_1:def 2;

        end;

        then for e be object st e in the carrier of L holds (f19 . e) = (f29 . e);

        hence f1 = f2 by FUNCT_2: 12;

      end;

    end

    theorem :: LATTICE5:14

    

     Th14: for d be distance_function of A, L holds ( alpha d) is meet-preserving

    proof

      let d be distance_function of A, L;

      let a,b be Element of L;

      set f = ( alpha d);

      

       A1: ex_inf_of ((f .: {a, b}),( EqRelLATT A)) by YELLOW_0: 17;

      consider E3 be Equivalence_Relation of A such that

       A2: E3 = (f . (a "/\" b)) and

       A3: for x,y be Element of A holds [x, y] in E3 iff (d . (x,y)) <= (a "/\" b) by Def8;

      consider E2 be Equivalence_Relation of A such that

       A4: E2 = (f . b) and

       A5: for x,y be Element of A holds [x, y] in E2 iff (d . (x,y)) <= b by Def8;

      consider E1 be Equivalence_Relation of A such that

       A6: E1 = (f . a) and

       A7: for x,y be Element of A holds [x, y] in E1 iff (d . (x,y)) <= a by Def8;

      

       A8: for x,y be Element of A holds [x, y] in (E1 /\ E2) iff [x, y] in E3

      proof

        let x,y be Element of A;

        hereby

          assume

           A9: [x, y] in (E1 /\ E2);

          then [x, y] in E2 by XBOOLE_0:def 4;

          then

           A10: (d . (x,y)) <= b by A5;

           [x, y] in E1 by A9, XBOOLE_0:def 4;

          then (d . (x,y)) <= a by A7;

          then (d . (x,y)) <= (a "/\" b) by A10, YELLOW_0: 23;

          hence [x, y] in E3 by A3;

        end;

        assume [x, y] in E3;

        then

         A11: (d . (x,y)) <= (a "/\" b) by A3;

        (a "/\" b) <= b by YELLOW_0: 23;

        then (d . (x,y)) <= b by A11, ORDERS_2: 3;

        then

         A12: [x, y] in E2 by A5;

        (a "/\" b) <= a by YELLOW_0: 23;

        then (d . (x,y)) <= a by A11, ORDERS_2: 3;

        then [x, y] in E1 by A7;

        hence thesis by A12, XBOOLE_0:def 4;

      end;

      

       A13: for x,y be object holds [x, y] in (E1 /\ E2) iff [x, y] in E3

      proof

        let x,y be object;

        (( field E1) /\ ( field E2)) = (A /\ ( field E2)) by EQREL_1: 9

        .= (A /\ A) by EQREL_1: 9

        .= A;

        then

         A14: ( field (E1 /\ E2)) c= A by RELAT_1: 19;

        hereby

          assume

           A15: [x, y] in (E1 /\ E2);

          then x in ( field (E1 /\ E2)) & y in ( field (E1 /\ E2)) by RELAT_1: 15;

          then

          reconsider x9 = x, y9 = y as Element of A by A14;

           [x9, y9] in E3 by A8, A15;

          hence [x, y] in E3;

        end;

        assume

         A16: [x, y] in E3;

        ( field E3) = A by EQREL_1: 9;

        then

        reconsider x9 = x, y9 = y as Element of A by A16, RELAT_1: 15;

         [x9, y9] in (E1 /\ E2) by A8, A16;

        hence thesis;

      end;

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

      

      then ( inf (f .: {a, b})) = ( inf {(f . a), (f . b)}) by FUNCT_1: 60

      .= ((f . a) "/\" (f . b)) by YELLOW_0: 40

      .= (E1 /\ E2) by A6, A4, Th8

      .= (f . (a "/\" b)) by A2, A13, RELAT_1:def 2

      .= (f . ( inf {a, b})) by YELLOW_0: 40;

      hence thesis by A1;

    end;

    theorem :: LATTICE5:15

    

     Th15: for d be distance_function of A, L st d is onto holds ( alpha d) is one-to-one

    proof

      let d be distance_function of A, L;

      set f = ( alpha d);

      assume d is onto;

      then

       A1: ( rng d) = the carrier of L by FUNCT_2:def 3;

      for a,b be Element of L st (f . a) = (f . b) holds a = b

      proof

        let a,b be Element of L;

        assume

         A2: (f . a) = (f . b);

        consider z1 be object such that

         A3: z1 in [:A, A:] and

         A4: (d . z1) = a by A1, FUNCT_2: 11;

        consider x1,y1 be object such that

         A5: x1 in A & y1 in A and

         A6: z1 = [x1, y1] by A3, ZFMISC_1:def 2;

        reconsider x1, y1 as Element of A by A5;

        consider z2 be object such that

         A7: z2 in [:A, A:] and

         A8: (d . z2) = b by A1, FUNCT_2: 11;

        consider x2,y2 be object such that

         A9: x2 in A & y2 in A and

         A10: z2 = [x2, y2] by A7, ZFMISC_1:def 2;

        reconsider x2, y2 as Element of A by A9;

        consider E1 be Equivalence_Relation of A such that

         A11: E1 = (f . a) and

         A12: for x,y be Element of A holds [x, y] in E1 iff (d . (x,y)) <= a by Def8;

        consider E2 be Equivalence_Relation of A such that

         A13: E2 = (f . b) and

         A14: for x,y be Element of A holds [x, y] in E2 iff (d . (x,y)) <= b by Def8;

        

         A15: (d . (x2,y2)) = b by A8, A10;

        then [x2, y2] in E2 by A14;

        then

         A16: b <= a by A2, A15, A11, A12, A13;

        

         A17: (d . (x1,y1)) = a by A4, A6;

        then [x1, y1] in E1 by A12;

        then a <= b by A2, A17, A11, A13, A14;

        hence thesis by A16, ORDERS_2: 2;

      end;

      hence thesis by WAYBEL_1:def 1;

    end;

    begin

    definition

      let A be set;

      :: LATTICE5:def9

      func new_set A -> set equals (A \/ { {A}, { {A}}, { { {A}}}});

      correctness ;

    end

    registration

      let A be set;

      cluster ( new_set A) -> non empty;

      coherence ;

    end

    definition

      let A, L;

      let d be BiFunction of A, L;

      let q be Element of [:A, A, the carrier of L, the carrier of L:];

      :: LATTICE5:def10

      func new_bi_fun (d,q) -> BiFunction of ( new_set A), L means

      : Def10: (for u,v be Element of A holds (it . (u,v)) = (d . (u,v))) & (it . ( {A}, {A})) = ( Bottom L) & (it . ( { {A}}, { {A}})) = ( Bottom L) & (it . ( { { {A}}}, { { {A}}})) = ( Bottom L) & (it . ( { {A}}, { { {A}}})) = (q `3_4 ) & (it . ( { { {A}}}, { {A}})) = (q `3_4 ) & (it . ( {A}, { {A}})) = (q `4_4 ) & (it . ( { {A}}, {A})) = (q `4_4 ) & (it . ( {A}, { { {A}}})) = ((q `3_4 ) "\/" (q `4_4 )) & (it . ( { { {A}}}, {A})) = ((q `3_4 ) "\/" (q `4_4 )) & for u be Element of A holds (it . (u, {A})) = ((d . (u,(q `1_4 ))) "\/" (q `3_4 )) & (it . ( {A},u)) = ((d . (u,(q `1_4 ))) "\/" (q `3_4 )) & (it . (u, { {A}})) = (((d . (u,(q `1_4 ))) "\/" (q `3_4 )) "\/" (q `4_4 )) & (it . ( { {A}},u)) = (((d . (u,(q `1_4 ))) "\/" (q `3_4 )) "\/" (q `4_4 )) & (it . (u, { { {A}}})) = ((d . (u,(q `2_4 ))) "\/" (q `4_4 )) & (it . ( { { {A}}},u)) = ((d . (u,(q `2_4 ))) "\/" (q `4_4 ));

      existence

      proof

        reconsider a = (q `3_4 ), b = (q `4_4 ) as Element of L;

        set x = (q `1_4 ), y = (q `2_4 );

        defpred X[ Element of ( new_set A), Element of ( new_set A), Element of L] means ($1 in A & $2 in A implies $3 = (d . ($1,$2))) & ($1 = { {A}} & $2 = { { {A}}} or $2 = { {A}} & $1 = { { {A}}} implies $3 = a) & ($1 = {A} & $2 = { {A}} or $2 = {A} & $1 = { {A}} implies $3 = b) & ($1 = {A} & $2 = { { {A}}} or $2 = {A} & $1 = { { {A}}} implies $3 = (a "\/" b)) & (($1 = {A} or $1 = { {A}} or $1 = { { {A}}}) & $2 = $1 implies $3 = ( Bottom L)) & ($1 in A & $2 = {A} implies ex p9 be Element of A st p9 = $1 & $3 = ((d . (p9,x)) "\/" a)) & ($1 in A & $2 = { {A}} implies ex p9 be Element of A st p9 = $1 & $3 = (((d . (p9,x)) "\/" a) "\/" b)) & ($1 in A & $2 = { { {A}}} implies ex p9 be Element of A st p9 = $1 & $3 = ((d . (p9,y)) "\/" b)) & ($2 in A & $1 = {A} implies ex q9 be Element of A st q9 = $2 & $3 = ((d . (q9,x)) "\/" a)) & ($2 in A & $1 = { {A}} implies ex q9 be Element of A st q9 = $2 & $3 = (((d . (q9,x)) "\/" a) "\/" b)) & ($2 in A & $1 = { { {A}}} implies ex q9 be Element of A st q9 = $2 & $3 = ((d . (q9,y)) "\/" b));

         { {A}} in { {A}, { {A}}, { { {A}}}} by ENUMSET1:def 1;

        then

         A1: { {A}} in ( new_set A) by XBOOLE_0:def 3;

        

         A2: for p,q be Element of ( new_set A) holds ex r be Element of L st X[p, q, r]

        proof

          let p,q be Element of ( new_set A);

          

           A3: p in A or p in { {A}, { {A}}, { { {A}}}} by XBOOLE_0:def 3;

          

           A4: q in A or q in { {A}, { {A}}, { { {A}}}} by XBOOLE_0:def 3;

          

           A5: (p = {A} or p = { {A}} or p = { { {A}}}) & p = q iff p = {A} & q = {A} or p = { {A}} & q = { {A}} or p = { { {A}}} & q = { { {A}}};

          

           A6: not {A} in A by TARSKI:def 1;

          

           A7: { {A}} <> { { {A}}}

          proof

            assume { {A}} = { { {A}}};

            then { {A}} in { {A}} by TARSKI:def 1;

            hence contradiction;

          end;

          

           A8: not { { {A}}} in A

          proof

            

             A9: { {A}} in { { {A}}} by TARSKI:def 1;

            

             A10: A in {A} & {A} in { {A}} by TARSKI:def 1;

            assume { { {A}}} in A;

            hence contradiction by A10, A9, XREGULAR: 8;

          end;

          

           A11: {A} <> { { {A}}}

          proof

            assume {A} = { { {A}}};

            then { {A}} in {A} by TARSKI:def 1;

            hence contradiction by TARSKI:def 1;

          end;

          

           A12: not { {A}} in A

          proof

            

             A13: A in {A} & {A} in { {A}} by TARSKI:def 1;

            assume { {A}} in A;

            hence contradiction by A13, XREGULAR: 7;

          end;

          per cases by A3, A4, A5, ENUMSET1:def 1;

            suppose p in A & q in A;

            then

            reconsider p9 = p, q9 = q as Element of A;

            take (d . (p9,q9));

            thus thesis by A6, A12, A8;

          end;

            suppose

             A14: p = { {A}} & q = { { {A}}} or q = { {A}} & p = { { {A}}};

            take a;

            thus thesis by A7, A11, A12, A8, A14;

          end;

            suppose

             A15: p = {A} & q = { {A}} or q = {A} & p = { {A}};

            take b;

            thus thesis by A7, A11, A12, A15, TARSKI:def 1;

          end;

            suppose

             A16: p = {A} & q = { { {A}}} or q = {A} & p = { { {A}}};

            take (a "\/" b);

            thus thesis by A7, A11, A8, A16, TARSKI:def 1;

          end;

            suppose

             A17: (p = {A} or p = { {A}} or p = { { {A}}}) & q = p;

            take ( Bottom L);

            thus thesis by A7, A11, A12, A8, A17, TARSKI:def 1;

          end;

            suppose

             A18: p in A & q = {A};

            then

            reconsider p9 = p as Element of A;

            take ((d . (p9,x)) "\/" a);

            thus thesis by A11, A12, A8, A18, TARSKI:def 1;

          end;

            suppose

             A19: p in A & q = { {A}};

            then

            reconsider p9 = p as Element of A;

            take (((d . (p9,x)) "\/" a) "\/" b);

            thus thesis by A7, A12, A8, A19, TARSKI:def 1;

          end;

            suppose

             A20: p in A & q = { { {A}}};

            then

            reconsider p9 = p as Element of A;

            take ((d . (p9,y)) "\/" b);

            thus thesis by A7, A11, A12, A8, A20, TARSKI:def 1;

          end;

            suppose

             A21: q in A & p = {A};

            then

            reconsider q9 = q as Element of A;

            take ((d . (q9,x)) "\/" a);

            thus thesis by A11, A12, A8, A21, TARSKI:def 1;

          end;

            suppose

             A22: q in A & p = { {A}};

            then

            reconsider q9 = q as Element of A;

            take (((d . (q9,x)) "\/" a) "\/" b);

            thus thesis by A7, A12, A8, A22, TARSKI:def 1;

          end;

            suppose

             A23: q in A & p = { { {A}}};

            then

            reconsider q9 = q as Element of A;

            take ((d . (q9,y)) "\/" b);

            thus thesis by A7, A11, A12, A8, A23, TARSKI:def 1;

          end;

        end;

        consider f be Function of [:( new_set A), ( new_set A):], the carrier of L such that

         A24: for p,q be Element of ( new_set A) holds X[p, q, (f . (p,q))] from BINOP_1:sch 3( A2);

         { { {A}}} in { {A}, { {A}}, { { {A}}}} by ENUMSET1:def 1;

        then

         A25: { { {A}}} in ( new_set A) by XBOOLE_0:def 3;

        reconsider f as BiFunction of ( new_set A), L;

         {A} in { {A}, { {A}}, { { {A}}}} by ENUMSET1:def 1;

        then

         A26: {A} in ( new_set A) by XBOOLE_0:def 3;

        

         A27: for u be Element of A holds (f . ( {A},u)) = ((d . (u,x)) "\/" a) & (f . ( { {A}},u)) = (((d . (u,x)) "\/" a) "\/" b) & (f . ( { { {A}}},u)) = ((d . (u,y)) "\/" b)

        proof

          let u be Element of A;

          reconsider u9 = u as Element of ( new_set A) by XBOOLE_0:def 3;

          ex u1 be Element of A st u1 = u9 & (f . ( {A},u9)) = ((d . (u1,x)) "\/" a) by A26, A24;

          hence (f . ( {A},u)) = ((d . (u,x)) "\/" a);

          ex u2 be Element of A st u2 = u9 & (f . ( { {A}},u9)) = (((d . (u2,x)) "\/" a) "\/" b) by A1, A24;

          hence (f . ( { {A}},u)) = (((d . (u,x)) "\/" a) "\/" b);

          ex u3 be Element of A st u3 = u9 & (f . ( { { {A}}},u9)) = ((d . (u3,y)) "\/" b) by A25, A24;

          hence thesis;

        end;

        take f;

        

         A28: for u,v be Element of A holds (f . (u,v)) = (d . (u,v))

        proof

          let u,v be Element of A;

          reconsider u9 = u, v9 = v as Element of ( new_set A) by XBOOLE_0:def 3;

          

          thus (f . (u,v)) = (f . (u9,v9))

          .= (d . (u,v)) by A24;

        end;

        for u be Element of A holds (f . (u, {A})) = ((d . (u,x)) "\/" a) & (f . (u, { {A}})) = (((d . (u,x)) "\/" a) "\/" b) & (f . (u, { { {A}}})) = ((d . (u,y)) "\/" b)

        proof

          let u be Element of A;

          reconsider u9 = u as Element of ( new_set A) by XBOOLE_0:def 3;

          ex u1 be Element of A st u1 = u9 & (f . (u9, {A})) = ((d . (u1,x)) "\/" a) by A26, A24;

          hence (f . (u, {A})) = ((d . (u,x)) "\/" a);

          ex u2 be Element of A st u2 = u9 & (f . (u9, { {A}})) = (((d . (u2,x)) "\/" a) "\/" b) by A1, A24;

          hence (f . (u, { {A}})) = (((d . (u,x)) "\/" a) "\/" b);

          ex u3 be Element of A st u3 = u9 & (f . (u9, { { {A}}})) = ((d . (u3,y)) "\/" b) by A25, A24;

          hence thesis;

        end;

        hence thesis by A26, A1, A25, A24, A28, A27;

      end;

      uniqueness

      proof

        set x = (q `1_4 ), y = (q `2_4 ), a = (q `3_4 ), b = (q `4_4 );

        let f1,f2 be BiFunction of ( new_set A), L such that

         A29: for u,v be Element of A holds (f1 . (u,v)) = (d . (u,v)) and

         A30: (f1 . ( {A}, {A})) = ( Bottom L) and

         A31: (f1 . ( { {A}}, { {A}})) = ( Bottom L) and

         A32: (f1 . ( { { {A}}}, { { {A}}})) = ( Bottom L) and

         A33: (f1 . ( { {A}}, { { {A}}})) = a and

         A34: (f1 . ( { { {A}}}, { {A}})) = a and

         A35: (f1 . ( {A}, { {A}})) = b and

         A36: (f1 . ( { {A}}, {A})) = b and

         A37: (f1 . ( {A}, { { {A}}})) = (a "\/" b) and

         A38: (f1 . ( { { {A}}}, {A})) = (a "\/" b) and

         A39: for u be Element of A holds (f1 . (u, {A})) = ((d . (u,x)) "\/" a) & (f1 . ( {A},u)) = ((d . (u,x)) "\/" a) & (f1 . (u, { {A}})) = (((d . (u,x)) "\/" a) "\/" b) & (f1 . ( { {A}},u)) = (((d . (u,x)) "\/" a) "\/" b) & (f1 . (u, { { {A}}})) = ((d . (u,y)) "\/" b) & (f1 . ( { { {A}}},u)) = ((d . (u,y)) "\/" b) and

         A40: for u,v be Element of A holds (f2 . (u,v)) = (d . (u,v)) and

         A41: (f2 . ( {A}, {A})) = ( Bottom L) and

         A42: (f2 . ( { {A}}, { {A}})) = ( Bottom L) and

         A43: (f2 . ( { { {A}}}, { { {A}}})) = ( Bottom L) and

         A44: (f2 . ( { {A}}, { { {A}}})) = a and

         A45: (f2 . ( { { {A}}}, { {A}})) = a and

         A46: (f2 . ( {A}, { {A}})) = b and

         A47: (f2 . ( { {A}}, {A})) = b and

         A48: (f2 . ( {A}, { { {A}}})) = (a "\/" b) and

         A49: (f2 . ( { { {A}}}, {A})) = (a "\/" b) and

         A50: for u be Element of A holds (f2 . (u, {A})) = ((d . (u,x)) "\/" a) & (f2 . ( {A},u)) = ((d . (u,x)) "\/" a) & (f2 . (u, { {A}})) = (((d . (u,x)) "\/" a) "\/" b) & (f2 . ( { {A}},u)) = (((d . (u,x)) "\/" a) "\/" b) & (f2 . (u, { { {A}}})) = ((d . (u,y)) "\/" b) & (f2 . ( { { {A}}},u)) = ((d . (u,y)) "\/" b);

        now

          let p,q be Element of ( new_set A);

          

           A51: p in A or p in { {A}, { {A}}, { { {A}}}} by XBOOLE_0:def 3;

          

           A52: q in A or q in { {A}, { {A}}, { { {A}}}} by XBOOLE_0:def 3;

          per cases by A51, A52, ENUMSET1:def 1;

            suppose

             A53: p in A & q in A;

            

            hence (f1 . (p,q)) = (d . (p,q)) by A29

            .= (f2 . (p,q)) by A40, A53;

          end;

            suppose

             A54: p in A & q = {A};

            then

            reconsider p9 = p as Element of A;

            

            thus (f1 . (p,q)) = ((d . (p9,x)) "\/" a) by A39, A54

            .= (f2 . (p,q)) by A50, A54;

          end;

            suppose

             A55: p in A & q = { {A}};

            then

            reconsider p9 = p as Element of A;

            

            thus (f1 . (p,q)) = (((d . (p9,x)) "\/" a) "\/" b) by A39, A55

            .= (f2 . (p,q)) by A50, A55;

          end;

            suppose

             A56: p in A & q = { { {A}}};

            then

            reconsider p9 = p as Element of A;

            

            thus (f1 . (p,q)) = ((d . (p9,y)) "\/" b) by A39, A56

            .= (f2 . (p,q)) by A50, A56;

          end;

            suppose

             A57: p = {A} & q in A;

            then

            reconsider q9 = q as Element of A;

            

            thus (f1 . (p,q)) = ((d . (q9,x)) "\/" a) by A39, A57

            .= (f2 . (p,q)) by A50, A57;

          end;

            suppose p = {A} & q = {A};

            hence (f1 . (p,q)) = (f2 . (p,q)) by A30, A41;

          end;

            suppose p = {A} & q = { {A}};

            hence (f1 . (p,q)) = (f2 . (p,q)) by A35, A46;

          end;

            suppose p = {A} & q = { { {A}}};

            hence (f1 . (p,q)) = (f2 . (p,q)) by A37, A48;

          end;

            suppose

             A58: p = { {A}} & q in A;

            then

            reconsider q9 = q as Element of A;

            

            thus (f1 . (p,q)) = (((d . (q9,x)) "\/" a) "\/" b) by A39, A58

            .= (f2 . (p,q)) by A50, A58;

          end;

            suppose p = { {A}} & q = {A};

            hence (f1 . (p,q)) = (f2 . (p,q)) by A36, A47;

          end;

            suppose p = { {A}} & q = { {A}};

            hence (f1 . (p,q)) = (f2 . (p,q)) by A31, A42;

          end;

            suppose p = { {A}} & q = { { {A}}};

            hence (f1 . (p,q)) = (f2 . (p,q)) by A33, A44;

          end;

            suppose

             A59: p = { { {A}}} & q in A;

            then

            reconsider q9 = q as Element of A;

            

            thus (f1 . (p,q)) = ((d . (q9,y)) "\/" b) by A39, A59

            .= (f2 . (p,q)) by A50, A59;

          end;

            suppose p = { { {A}}} & q = {A};

            hence (f1 . (p,q)) = (f2 . (p,q)) by A38, A49;

          end;

            suppose p = { { {A}}} & q = { {A}};

            hence (f1 . (p,q)) = (f2 . (p,q)) by A34, A45;

          end;

            suppose p = { { {A}}} & q = { { {A}}};

            hence (f1 . (p,q)) = (f2 . (p,q)) by A32, A43;

          end;

        end;

        hence f1 = f2;

      end;

    end

    theorem :: LATTICE5:16

    

     Th16: for d be BiFunction of A, L st d is zeroed holds for q be Element of [:A, A, the carrier of L, the carrier of L:] holds ( new_bi_fun (d,q)) is zeroed

    proof

      let d be BiFunction of A, L;

      assume

       A1: d is zeroed;

      let q be Element of [:A, A, the carrier of L, the carrier of L:];

      set f = ( new_bi_fun (d,q));

      for u be Element of ( new_set A) holds (f . (u,u)) = ( Bottom L)

      proof

        let u be Element of ( new_set A);

        

         A2: u in A or u in { {A}, { {A}}, { { {A}}}} by XBOOLE_0:def 3;

        per cases by A2, ENUMSET1:def 1;

          suppose u in A;

          then

          reconsider u9 = u as Element of A;

          

          thus (f . (u,u)) = (d . (u9,u9)) by Def10

          .= ( Bottom L) by A1;

        end;

          suppose u = {A} or u = { {A}} or u = { { {A}}};

          hence thesis by Def10;

        end;

      end;

      hence thesis;

    end;

    theorem :: LATTICE5:17

    

     Th17: for d be BiFunction of A, L st d is symmetric holds for q be Element of [:A, A, the carrier of L, the carrier of L:] holds ( new_bi_fun (d,q)) is symmetric

    proof

      let d be BiFunction of A, L;

      assume

       A1: d is symmetric;

      let q be Element of [:A, A, the carrier of L, the carrier of L:];

      set f = ( new_bi_fun (d,q)), x = (q `1_4 ), y = (q `2_4 ), a = (q `3_4 ), b = (q `4_4 );

      let p,q be Element of ( new_set A);

      

       A2: p in A or p in { {A}, { {A}}, { { {A}}}} by XBOOLE_0:def 3;

      

       A3: q in A or q in { {A}, { {A}}, { { {A}}}} by XBOOLE_0:def 3;

      per cases by A2, A3, ENUMSET1:def 1;

        suppose p in A & q in A;

        then

        reconsider p9 = p, q9 = q as Element of A;

        

        thus (f . (p,q)) = (d . (p9,q9)) by Def10

        .= (d . (q9,p9)) by A1

        .= (f . (q,p)) by Def10;

      end;

        suppose

         A4: p in A & q = {A};

        then

        reconsider p9 = p as Element of A;

        

        thus (f . (p,q)) = ((d . (p9,x)) "\/" a) by A4, Def10

        .= (f . (q,p)) by A4, Def10;

      end;

        suppose

         A5: p in A & q = { {A}};

        then

        reconsider p9 = p as Element of A;

        

        thus (f . (p,q)) = (((d . (p9,x)) "\/" a) "\/" b) by A5, Def10

        .= (f . (q,p)) by A5, Def10;

      end;

        suppose

         A6: p in A & q = { { {A}}};

        then

        reconsider p9 = p as Element of A;

        

        thus (f . (p,q)) = ((d . (p9,y)) "\/" b) by A6, Def10

        .= (f . (q,p)) by A6, Def10;

      end;

        suppose

         A7: p = {A} & q in A;

        then

        reconsider q9 = q as Element of A;

        

        thus (f . (p,q)) = ((d . (q9,x)) "\/" a) by A7, Def10

        .= (f . (q,p)) by A7, Def10;

      end;

        suppose p = {A} & q = {A};

        hence thesis;

      end;

        suppose

         A8: p = {A} & q = { {A}};

        

        hence (f . (p,q)) = b by Def10

        .= (f . (q,p)) by A8, Def10;

      end;

        suppose

         A9: p = {A} & q = { { {A}}};

        

        hence (f . (p,q)) = (a "\/" b) by Def10

        .= (f . (q,p)) by A9, Def10;

      end;

        suppose

         A10: p = { {A}} & q in A;

        then

        reconsider q9 = q as Element of A;

        

        thus (f . (p,q)) = (((d . (q9,x)) "\/" a) "\/" b) by A10, Def10

        .= (f . (q,p)) by A10, Def10;

      end;

        suppose

         A11: p = { {A}} & q = {A};

        

        hence (f . (p,q)) = b by Def10

        .= (f . (q,p)) by A11, Def10;

      end;

        suppose p = { {A}} & q = { {A}};

        hence thesis;

      end;

        suppose

         A12: p = { {A}} & q = { { {A}}};

        

        hence (f . (p,q)) = a by Def10

        .= (f . (q,p)) by A12, Def10;

      end;

        suppose

         A13: p = { { {A}}} & q in A;

        then

        reconsider q9 = q as Element of A;

        

        thus (f . (p,q)) = ((d . (q9,y)) "\/" b) by A13, Def10

        .= (f . (q,p)) by A13, Def10;

      end;

        suppose

         A14: p = { { {A}}} & q = {A};

        

        hence (f . (p,q)) = (a "\/" b) by Def10

        .= (f . (q,p)) by A14, Def10;

      end;

        suppose

         A15: p = { { {A}}} & q = { {A}};

        

        hence (f . (p,q)) = a by Def10

        .= (f . (q,p)) by A15, Def10;

      end;

        suppose p = { { {A}}} & q = { { {A}}};

        hence thesis;

      end;

    end;

    theorem :: LATTICE5:18

    

     Th18: for d be BiFunction of A, L st d is symmetric & d is u.t.i. holds for q be Element of [:A, A, the carrier of L, the carrier of L:] st (d . ((q `1_4 ),(q `2_4 ))) <= ((q `3_4 ) "\/" (q `4_4 )) holds ( new_bi_fun (d,q)) is u.t.i.

    proof

      let d be BiFunction of A, L;

      assume that

       A1: d is symmetric and

       A2: d is u.t.i.;

      reconsider B = { {A}, { {A}}, { { {A}}}} as non empty set;

      let q be Element of [:A, A, the carrier of L, the carrier of L:];

      set x = (q `1_4 ), y = (q `2_4 ), f = ( new_bi_fun (d,q));

      reconsider a = (q `3_4 ), b = (q `4_4 ) as Element of L;

      

       A3: for p,q,u be Element of ( new_set A) st p in A & q in B & u in A holds (f . (p,u)) <= ((f . (p,q)) "\/" (f . (q,u)))

      proof

        let p,q,u be Element of ( new_set A);

        assume

         A4: p in A & q in B & u in A;

        per cases by A4, ENUMSET1:def 1;

          suppose

           A5: p in A & u in A & q = {A};

          then

          reconsider p9 = p, u9 = u as Element of A;

          (d . (p9,u9)) <= ((d . (p9,x)) "\/" (d . (x,u9))) by A2;

          then

           A6: ((d . (p9,x)) "\/" (d . (u9,x))) <= (((d . (p9,x)) "\/" (d . (u9,x))) "\/" a) & (d . (p9,u9)) <= ((d . (p9,x)) "\/" (d . (u9,x))) by A1, YELLOW_0: 22;

          (((d . (p9,x)) "\/" (d . (u9,x))) "\/" a) = ((d . (p9,x)) "\/" ((d . (u9,x)) "\/" a)) by LATTICE3: 14

          .= ((d . (p9,x)) "\/" ((d . (u9,x)) "\/" (a "\/" a))) by YELLOW_5: 1

          .= ((d . (p9,x)) "\/" (((d . (u9,x)) "\/" a) "\/" a)) by LATTICE3: 14

          .= (((d . (p9,x)) "\/" a) "\/" ((d . (u9,x)) "\/" a)) by LATTICE3: 14;

          then

           A7: (d . (p9,u9)) <= (((d . (p9,x)) "\/" a) "\/" ((d . (u9,x)) "\/" a)) by A6, ORDERS_2: 3;

          (f . (p,q)) = ((d . (p9,x)) "\/" a) & (f . (q,u)) = ((d . (u9,x)) "\/" a) by A5, Def10;

          hence thesis by A7, Def10;

        end;

          suppose

           A8: p in A & u in A & q = { {A}};

          then

          reconsider p9 = p, u9 = u as Element of A;

          (d . (p9,u9)) <= ((d . (p9,x)) "\/" (d . (x,u9))) by A2;

          then

           A9: ((d . (p9,x)) "\/" (d . (u9,x))) <= (((d . (p9,x)) "\/" (d . (u9,x))) "\/" (a "\/" b)) & (d . (p9,u9)) <= ((d . (p9,x)) "\/" (d . (u9,x))) by A1, YELLOW_0: 22;

          (((d . (p9,x)) "\/" (d . (u9,x))) "\/" (a "\/" b)) = ((d . (p9,x)) "\/" ((d . (u9,x)) "\/" (a "\/" b))) by LATTICE3: 14

          .= ((d . (p9,x)) "\/" ((d . (u9,x)) "\/" ((a "\/" b) "\/" (a "\/" b)))) by YELLOW_5: 1

          .= ((d . (p9,x)) "\/" (((d . (u9,x)) "\/" (a "\/" b)) "\/" (a "\/" b))) by LATTICE3: 14

          .= (((d . (p9,x)) "\/" (a "\/" b)) "\/" ((d . (u9,x)) "\/" (a "\/" b))) by LATTICE3: 14

          .= ((((d . (p9,x)) "\/" a) "\/" b) "\/" ((d . (u9,x)) "\/" (a "\/" b))) by LATTICE3: 14

          .= ((((d . (p9,x)) "\/" a) "\/" b) "\/" (((d . (u9,x)) "\/" a) "\/" b)) by LATTICE3: 14;

          then

           A10: (d . (p9,u9)) <= ((((d . (p9,x)) "\/" a) "\/" b) "\/" (((d . (u9,x)) "\/" a) "\/" b)) by A9, ORDERS_2: 3;

          (f . (p,q)) = (((d . (p9,x)) "\/" a) "\/" b) & (f . (q,u)) = (((d . (u9,x)) "\/" a) "\/" b) by A8, Def10;

          hence thesis by A10, Def10;

        end;

          suppose

           A11: p in A & u in A & q = { { {A}}};

          then

          reconsider p9 = p, u9 = u as Element of A;

          (d . (p9,u9)) <= ((d . (p9,y)) "\/" (d . (y,u9))) by A2;

          then

           A12: ((d . (p9,y)) "\/" (d . (u9,y))) <= (((d . (p9,y)) "\/" (d . (u9,y))) "\/" b) & (d . (p9,u9)) <= ((d . (p9,y)) "\/" (d . (u9,y))) by A1, YELLOW_0: 22;

          (((d . (p9,y)) "\/" (d . (u9,y))) "\/" b) = ((d . (p9,y)) "\/" ((d . (u9,y)) "\/" b)) by LATTICE3: 14

          .= ((d . (p9,y)) "\/" ((d . (u9,y)) "\/" (b "\/" b))) by YELLOW_5: 1

          .= ((d . (p9,y)) "\/" (((d . (u9,y)) "\/" b) "\/" b)) by LATTICE3: 14

          .= (((d . (p9,y)) "\/" b) "\/" ((d . (u9,y)) "\/" b)) by LATTICE3: 14;

          then

           A13: (d . (p9,u9)) <= (((d . (p9,y)) "\/" b) "\/" ((d . (u9,y)) "\/" b)) by A12, ORDERS_2: 3;

          (f . (p,q)) = ((d . (p9,y)) "\/" b) & (f . (q,u)) = ((d . (u9,y)) "\/" b) by A11, Def10;

          hence thesis by A13, Def10;

        end;

      end;

      assume

       A14: (d . ((q `1_4 ),(q `2_4 ))) <= ((q `3_4 ) "\/" (q `4_4 ));

      

       A15: for p,q,u be Element of ( new_set A) st p in B & q in B & u in A holds (f . (p,u)) <= ((f . (p,q)) "\/" (f . (q,u)))

      proof

        let p,q,u be Element of ( new_set A);

        assume that

         A16: p in B & q in B and

         A17: u in A;

        reconsider u9 = u as Element of A by A17;

        per cases by A16, A17, ENUMSET1:def 1;

          suppose

           A18: u in A & q = {A} & p = {A};

          

          then ((f . (p,q)) "\/" (f . (q,u))) = (( Bottom L) "\/" (f . (q,u))) by Def10

          .= (f . (p,u)) by A18, WAYBEL_1: 3;

          hence thesis;

        end;

          suppose

           A19: u in A & q = {A} & p = { {A}};

          

          then ((f . (p,q)) "\/" (f . (q,u))) = (b "\/" (f . (q,u))) by Def10

          .= (((d . (u9,x)) "\/" a) "\/" b) by A19, Def10;

          hence thesis by A19, Def10;

        end;

          suppose

           A20: u in A & q = {A} & p = { { {A}}};

          (b "\/" (a "\/" b)) = ((b "\/" b) "\/" a) by LATTICE3: 14

          .= (b "\/" a) by YELLOW_5: 1

          .= (b "\/" (a "\/" a)) by YELLOW_5: 1

          .= (a "\/" (a "\/" b)) by LATTICE3: 14;

          

          then

           A21: (((d . (u9,x)) "\/" b) "\/" (a "\/" b)) = ((d . (u9,x)) "\/" (a "\/" (a "\/" b))) by LATTICE3: 14

          .= ((a "\/" b) "\/" ((d . (u9,x)) "\/" a)) by LATTICE3: 14

          .= ((f . (p,q)) "\/" ((d . (u9,x)) "\/" a)) by A20, Def10;

          (d . (u9,y)) <= ((d . (u9,x)) "\/" (d . (x,y))) by A2;

          then

           A22: ((d . (u9,y)) "\/" b) <= (((d . (u9,x)) "\/" (d . (x,y))) "\/" b) by WAYBEL_1: 2;

          ((d . (u9,x)) "\/" b) <= ((d . (u9,x)) "\/" b);

          then

           A23: (((d . (u9,x)) "\/" (d . (x,y))) "\/" b) = (((d . (u9,x)) "\/" b) "\/" (d . (x,y))) & (((d . (u9,x)) "\/" b) "\/" (d . (x,y))) <= (((d . (u9,x)) "\/" b) "\/" (a "\/" b)) by A14, LATTICE3: 14, YELLOW_3: 3;

          (f . (p,u)) = ((d . (u9,y)) "\/" b) by A20, Def10;

          then (f . (p,u)) <= (((d . (u9,x)) "\/" b) "\/" (a "\/" b)) by A22, A23, ORDERS_2: 3;

          hence thesis by A20, A21, Def10;

        end;

          suppose

           A24: u in A & q = { {A}} & p = {A};

          

          then ((f . (p,q)) "\/" (f . (q,u))) = (b "\/" (f . (q,u))) by Def10

          .= (b "\/" (((d . (u9,x)) "\/" a) "\/" b)) by A24, Def10

          .= (b "\/" (b "\/" (f . (p,u)))) by A24, Def10

          .= ((b "\/" b) "\/" (f . (p,u))) by LATTICE3: 14

          .= (b "\/" (f . (p,u))) by YELLOW_5: 1;

          hence thesis by YELLOW_0: 22;

        end;

          suppose

           A25: u in A & q = { {A}} & p = { {A}};

          

          then ((f . (p,q)) "\/" (f . (q,u))) = (( Bottom L) "\/" (f . (q,u))) by Def10

          .= (f . (p,u)) by A25, WAYBEL_1: 3;

          hence thesis;

        end;

          suppose

           A26: u in A & q = { {A}} & p = { { {A}}};

          (b "\/" (a "\/" b)) = ((b "\/" b) "\/" a) by LATTICE3: 14

          .= (b "\/" a) by YELLOW_5: 1

          .= (b "\/" (a "\/" a)) by YELLOW_5: 1

          .= ((a "\/" b) "\/" a) by LATTICE3: 14;

          

          then

           A27: (((d . (u9,x)) "\/" b) "\/" (a "\/" b)) = ((d . (u9,x)) "\/" ((a "\/" b) "\/" a)) by LATTICE3: 14

          .= (((d . (u9,x)) "\/" (a "\/" b)) "\/" a) by LATTICE3: 14

          .= ((((d . (u9,x)) "\/" a) "\/" b) "\/" a) by LATTICE3: 14

          .= ((f . (p,q)) "\/" (((d . (u9,x)) "\/" a) "\/" b)) by A26, Def10;

          ((d . (u9,x)) "\/" b) <= ((d . (u9,x)) "\/" b);

          then

           A28: (((d . (u9,x)) "\/" (d . (x,y))) "\/" b) = (((d . (u9,x)) "\/" b) "\/" (d . (x,y))) & (((d . (u9,x)) "\/" b) "\/" (d . (x,y))) <= (((d . (u9,x)) "\/" b) "\/" (a "\/" b)) by A14, LATTICE3: 14, YELLOW_3: 3;

          (d . (u9,y)) <= ((d . (u9,x)) "\/" (d . (x,y))) by A2;

          then

           A29: ((d . (u9,y)) "\/" b) <= (((d . (u9,x)) "\/" (d . (x,y))) "\/" b) by WAYBEL_1: 2;

          (f . (p,u)) = ((d . (u9,y)) "\/" b) by A26, Def10;

          then (f . (p,u)) <= (((d . (u9,x)) "\/" b) "\/" (a "\/" b)) by A29, A28, ORDERS_2: 3;

          hence thesis by A26, A27, Def10;

        end;

          suppose

           A30: u in A & q = { { {A}}} & p = {A};

          

           A31: (a "\/" (a "\/" b)) = ((a "\/" a) "\/" b) by LATTICE3: 14

          .= (a "\/" b) by YELLOW_5: 1

          .= (a "\/" (b "\/" b)) by YELLOW_5: 1

          .= (b "\/" (a "\/" b)) by LATTICE3: 14;

          

           A32: ((a "\/" (d . (u9,y))) "\/" (a "\/" b)) = ((d . (u9,y)) "\/" (a "\/" (a "\/" b))) by LATTICE3: 14

          .= (((d . (u9,y)) "\/" b) "\/" (a "\/" b)) by A31, LATTICE3: 14

          .= ((f . (p,q)) "\/" ((d . (u9,y)) "\/" b)) by A30, Def10;

          (a "\/" (d . (u9,y))) <= (a "\/" (d . (u9,y)));

          then

           A33: ((a "\/" (d . (u9,y))) "\/" (d . (x,y))) <= ((a "\/" (d . (u9,y))) "\/" (a "\/" b)) by A14, YELLOW_3: 3;

          (d . (u9,x)) <= ((d . (u9,y)) "\/" (d . (y,x))) by A2;

          then

           A34: ((d . (u9,x)) "\/" a) <= (((d . (u9,y)) "\/" (d . (y,x))) "\/" a) by WAYBEL_1: 2;

          

           A35: (((d . (u9,y)) "\/" (d . (y,x))) "\/" a) = ((d . (y,x)) "\/" ((d . (u9,y)) "\/" a)) by LATTICE3: 14

          .= ((a "\/" (d . (u9,y))) "\/" (d . (x,y))) by A1;

          (f . (p,u)) = ((d . (u9,x)) "\/" a) by A30, Def10;

          then (f . (p,u)) <= ((a "\/" (d . (u9,y))) "\/" (a "\/" b)) by A34, A35, A33, ORDERS_2: 3;

          hence thesis by A30, A32, Def10;

        end;

          suppose

           A36: u in A & q = { { {A}}} & p = { {A}};

          

          then

           A37: (f . (p,u)) = (((d . (u9,x)) "\/" a) "\/" b) by Def10

          .= ((d . (u9,x)) "\/" (a "\/" b)) by LATTICE3: 14;

          ((a "\/" b) "\/" (d . (u9,y))) <= ((a "\/" b) "\/" (d . (u9,y)));

          then

           A38: (((a "\/" b) "\/" (d . (u9,y))) "\/" (d . (x,y))) <= (((a "\/" b) "\/" (d . (u9,y))) "\/" (a "\/" b)) by A14, YELLOW_3: 3;

          (d . (u9,x)) <= ((d . (u9,y)) "\/" (d . (y,x))) by A2;

          then

           A39: ((d . (u9,x)) "\/" (a "\/" b)) <= (((d . (u9,y)) "\/" (d . (y,x))) "\/" (a "\/" b)) by WAYBEL_1: 2;

          

           A40: (((d . (u9,y)) "\/" (d . (y,x))) "\/" (a "\/" b)) = (((a "\/" b) "\/" (d . (u9,y))) "\/" (d . (y,x))) by LATTICE3: 14

          .= (((a "\/" b) "\/" (d . (u9,y))) "\/" (d . (x,y))) by A1;

          ((f . (p,q)) "\/" (f . (q,u))) = (a "\/" (f . (q,u))) by A36, Def10

          .= (a "\/" (b "\/" (d . (u9,y)))) by A36, Def10

          .= ((a "\/" b) "\/" (d . (u9,y))) by LATTICE3: 14

          .= (((a "\/" b) "\/" (a "\/" b)) "\/" (d . (u9,y))) by YELLOW_5: 1

          .= ((a "\/" b) "\/" ((d . (u9,y)) "\/" (a "\/" b))) by LATTICE3: 14;

          hence thesis by A37, A39, A40, A38, ORDERS_2: 3;

        end;

          suppose

           A41: u in A & q = { { {A}}} & p = { { {A}}};

          

          then ((f . (p,q)) "\/" (f . (q,u))) = (( Bottom L) "\/" (f . (q,u))) by Def10

          .= (f . (p,u)) by A41, WAYBEL_1: 3;

          hence thesis;

        end;

      end;

      

       A42: for p,q,u be Element of ( new_set A) st p in B & q in A & u in A holds (f . (p,u)) <= ((f . (p,q)) "\/" (f . (q,u)))

      proof

        let p,q,u be Element of ( new_set A);

        assume that

         A43: p in B and

         A44: q in A & u in A;

        reconsider q9 = q, u9 = u as Element of A by A44;

        per cases by A43, A44, ENUMSET1:def 1;

          suppose

           A45: p = {A} & q in A & u in A;

          (d . (u9,x)) <= ((d . (u9,q9)) "\/" (d . (q9,x))) by A2;

          then (d . (u9,x)) <= ((d . (q9,u9)) "\/" (d . (q9,x))) by A1;

          then ((d . (u9,x)) "\/" a) <= (((d . (q9,x)) "\/" (d . (q9,u9))) "\/" a) by WAYBEL_1: 2;

          then

           A46: ((d . (u9,x)) "\/" a) <= (((d . (q9,x)) "\/" a) "\/" (d . (q9,u9))) by LATTICE3: 14;

          

           A47: (f . (q,u)) = (d . (q9,u9)) by Def10;

          (f . (p,q)) = ((d . (q9,x)) "\/" a) by A45, Def10;

          hence thesis by A45, A47, A46, Def10;

        end;

          suppose

           A48: p = { {A}} & q in A & u in A;

          (d . (u9,x)) <= ((d . (u9,q9)) "\/" (d . (q9,x))) by A2;

          then (d . (u9,x)) <= ((d . (q9,u9)) "\/" (d . (q9,x))) by A1;

          then ((d . (u9,x)) "\/" (a "\/" b)) <= (((d . (q9,x)) "\/" (d . (q9,u9))) "\/" (a "\/" b)) by WAYBEL_1: 2;

          then (((d . (u9,x)) "\/" a) "\/" b) <= (((d . (q9,x)) "\/" (d . (q9,u9))) "\/" (a "\/" b)) by LATTICE3: 14;

          then (((d . (u9,x)) "\/" a) "\/" b) <= (((d . (q9,x)) "\/" (a "\/" b)) "\/" (d . (q9,u9))) by LATTICE3: 14;

          then

           A49: (((d . (u9,x)) "\/" a) "\/" b) <= ((((d . (q9,x)) "\/" a) "\/" b) "\/" (d . (q9,u9))) by LATTICE3: 14;

          

           A50: (f . (q,u)) = (d . (q9,u9)) by Def10;

          (f . (p,q)) = (((d . (q9,x)) "\/" a) "\/" b) by A48, Def10;

          hence thesis by A48, A50, A49, Def10;

        end;

          suppose

           A51: p = { { {A}}} & q in A & u in A;

          (d . (u9,y)) <= ((d . (u9,q9)) "\/" (d . (q9,y))) by A2;

          then (d . (u9,y)) <= ((d . (q9,u9)) "\/" (d . (q9,y))) by A1;

          then ((d . (u9,y)) "\/" b) <= (((d . (q9,y)) "\/" (d . (q9,u9))) "\/" b) by WAYBEL_1: 2;

          then

           A52: ((d . (u9,y)) "\/" b) <= (((d . (q9,y)) "\/" b) "\/" (d . (q9,u9))) by LATTICE3: 14;

          

           A53: (f . (q,u)) = (d . (q9,u9)) by Def10;

          (f . (p,q)) = ((d . (q9,y)) "\/" b) by A51, Def10;

          hence thesis by A51, A53, A52, Def10;

        end;

      end;

      

       A54: for p,q,u be Element of ( new_set A) st p in A & q in A & u in B holds (f . (p,u)) <= ((f . (p,q)) "\/" (f . (q,u)))

      proof

        let p,q,u be Element of ( new_set A);

        assume

         A55: p in A & q in A & u in B;

        per cases by A55, ENUMSET1:def 1;

          suppose

           A56: p in A & q in A & u = {A};

          then

          reconsider p9 = p, q9 = q as Element of A;

          

           A57: (f . (p,q)) = (d . (p9,q9)) by Def10;

          (d . (p9,x)) <= ((d . (p9,q9)) "\/" (d . (q9,x))) by A2;

          then

           A58: ((d . (p9,x)) "\/" a) <= (((d . (p9,q9)) "\/" (d . (q9,x))) "\/" a) by WAYBEL_1: 2;

          (f . (p,u)) = ((d . (p9,x)) "\/" a) & (f . (q,u)) = ((d . (q9,x)) "\/" a) by A56, Def10;

          hence thesis by A57, A58, LATTICE3: 14;

        end;

          suppose

           A59: p in A & q in A & u = { {A}};

          then

          reconsider p9 = p, q9 = q as Element of A;

          

           A60: (f . (p,q)) = (d . (p9,q9)) by Def10;

          (d . (p9,x)) <= ((d . (p9,q9)) "\/" (d . (q9,x))) by A2;

          then ((d . (p9,x)) "\/" a) <= (((d . (p9,q9)) "\/" (d . (q9,x))) "\/" a) by WAYBEL_1: 2;

          then (((d . (p9,x)) "\/" a) "\/" b) <= ((((d . (p9,q9)) "\/" (d . (q9,x))) "\/" a) "\/" b) by WAYBEL_1: 2;

          then

           A61: (((d . (p9,x)) "\/" a) "\/" b) <= (((d . (p9,q9)) "\/" ((d . (q9,x)) "\/" a)) "\/" b) by LATTICE3: 14;

          (f . (p,u)) = (((d . (p9,x)) "\/" a) "\/" b) & (f . (q,u)) = (((d . (q9,x)) "\/" a) "\/" b) by A59, Def10;

          hence thesis by A60, A61, LATTICE3: 14;

        end;

          suppose

           A62: p in A & q in A & u = { { {A}}};

          then

          reconsider p9 = p, q9 = q as Element of A;

          

           A63: (f . (p,q)) = (d . (p9,q9)) by Def10;

          (d . (p9,y)) <= ((d . (p9,q9)) "\/" (d . (q9,y))) by A2;

          then

           A64: ((d . (p9,y)) "\/" b) <= (((d . (p9,q9)) "\/" (d . (q9,y))) "\/" b) by WAYBEL_1: 2;

          (f . (p,u)) = ((d . (p9,y)) "\/" b) & (f . (q,u)) = ((d . (q9,y)) "\/" b) by A62, Def10;

          hence thesis by A63, A64, LATTICE3: 14;

        end;

      end;

      

       A65: for p,q,u be Element of ( new_set A) st p in B & q in B & u in B holds (f . (p,u)) <= ((f . (p,q)) "\/" (f . (q,u)))

      proof

        let p,q,u be Element of ( new_set A);

        assume

         A66: p in B & q in B & u in B;

        per cases by A66, ENUMSET1:def 1;

          suppose

           A67: p = {A} & q = {A} & u = {A};

          ( Bottom L) <= ((f . (p,q)) "\/" (f . (q,u))) by YELLOW_0: 44;

          hence thesis by A67, Def10;

        end;

          suppose

           A68: p = {A} & q = {A} & u = { {A}};

          

          then ((f . (p,q)) "\/" (f . (q,u))) = (( Bottom L) "\/" (f . (p,u))) by Def10

          .= (( Bottom L) "\/" b) by A68, Def10

          .= b by WAYBEL_1: 3;

          hence thesis by A68, Def10;

        end;

          suppose

           A69: p = {A} & q = {A} & u = { { {A}}};

          

          then ((f . (p,q)) "\/" (f . (q,u))) = (( Bottom L) "\/" (f . (p,u))) by Def10

          .= (( Bottom L) "\/" (a "\/" b)) by A69, Def10

          .= (a "\/" b) by WAYBEL_1: 3;

          hence thesis by A69, Def10;

        end;

          suppose

           A70: p = {A} & q = { {A}} & u = {A};

          ( Bottom L) <= ((f . (p,q)) "\/" (f . (q,u))) by YELLOW_0: 44;

          hence thesis by A70, Def10;

        end;

          suppose

           A71: p = {A} & q = { {A}} & u = { {A}};

          

          then ((f . (p,q)) "\/" (f . (q,u))) = (b "\/" (f . (q,u))) by Def10

          .= (( Bottom L) "\/" b) by A71, Def10

          .= b by WAYBEL_1: 3;

          hence thesis by A71, Def10;

        end;

          suppose

           A72: p = {A} & q = { {A}} & u = { { {A}}};

          

          then ((f . (p,q)) "\/" (f . (q,u))) = (b "\/" (f . (q,u))) by Def10

          .= (a "\/" b) by A72, Def10;

          hence thesis by A72, Def10;

        end;

          suppose

           A73: p = {A} & q = { { {A}}} & u = {A};

          ( Bottom L) <= ((f . (p,q)) "\/" (f . (q,u))) by YELLOW_0: 44;

          hence thesis by A73, Def10;

        end;

          suppose

           A74: p = {A} & q = { { {A}}} & u = { {A}};

          then

           A75: (f . (p,u)) = b by Def10;

          ((f . (p,q)) "\/" (f . (q,u))) = ((a "\/" b) "\/" (f . (q,u))) by A74, Def10

          .= ((b "\/" a) "\/" a) by A74, Def10

          .= (b "\/" (a "\/" a)) by LATTICE3: 14

          .= (b "\/" a) by YELLOW_5: 1;

          hence thesis by A75, YELLOW_0: 22;

        end;

          suppose

           A76: p = {A} & q = { { {A}}} & u = { { {A}}};

          

          then ((f . (p,q)) "\/" (f . (q,u))) = ((a "\/" b) "\/" (f . (q,u))) by Def10

          .= (( Bottom L) "\/" (a "\/" b)) by A76, Def10

          .= (a "\/" b) by WAYBEL_1: 3

          .= (f . (p,q)) by A76, Def10;

          hence thesis by A76;

        end;

          suppose

           A77: p = { {A}} & q = {A} & u = {A};

          

          then ((f . (p,q)) "\/" (f . (q,u))) = (b "\/" (f . (q,u))) by Def10

          .= (( Bottom L) "\/" b) by A77, Def10

          .= b by WAYBEL_1: 3

          .= (f . (p,q)) by A77, Def10;

          hence thesis by A77;

        end;

          suppose

           A78: p = { {A}} & q = {A} & u = { {A}};

          ( Bottom L) <= ((f . (p,q)) "\/" (f . (q,u))) by YELLOW_0: 44;

          hence thesis by A78, Def10;

        end;

          suppose

           A79: p = { {A}} & q = {A} & u = { { {A}}};

          then

           A80: (f . (p,u)) = a by Def10;

          ((f . (p,q)) "\/" (f . (q,u))) = (b "\/" (f . (q,u))) by A79, Def10

          .= (b "\/" (b "\/" a)) by A79, Def10

          .= ((b "\/" b) "\/" a) by LATTICE3: 14

          .= (b "\/" a) by YELLOW_5: 1;

          hence thesis by A80, YELLOW_0: 22;

        end;

          suppose

           A81: p = { {A}} & q = { {A}} & u = {A};

          

          then ((f . (p,q)) "\/" (f . (q,u))) = (( Bottom L) "\/" (f . (p,u))) by Def10

          .= (( Bottom L) "\/" b) by A81, Def10

          .= b by WAYBEL_1: 3;

          hence thesis by A81, Def10;

        end;

          suppose

           A82: p = { {A}} & q = { {A}} & u = { {A}};

          ( Bottom L) <= ((f . (p,q)) "\/" (f . (q,u))) by YELLOW_0: 44;

          hence thesis by A82, Def10;

        end;

          suppose

           A83: p = { {A}} & q = { {A}} & u = { { {A}}};

          

          then ((f . (p,q)) "\/" (f . (q,u))) = (( Bottom L) "\/" (f . (p,u))) by Def10

          .= (( Bottom L) "\/" a) by A83, Def10

          .= a by WAYBEL_1: 3;

          hence thesis by A83, Def10;

        end;

          suppose

           A84: p = { {A}} & q = { { {A}}} & u = {A};

          then

           A85: (f . (p,u)) = b by Def10;

          ((f . (p,q)) "\/" (f . (q,u))) = (a "\/" (f . (q,u))) by A84, Def10

          .= (a "\/" (a "\/" b)) by A84, Def10

          .= ((a "\/" a) "\/" b) by LATTICE3: 14

          .= (a "\/" b) by YELLOW_5: 1;

          hence thesis by A85, YELLOW_0: 22;

        end;

          suppose

           A86: p = { {A}} & q = { { {A}}} & u = { {A}};

          ( Bottom L) <= ((f . (p,q)) "\/" (f . (q,u))) by YELLOW_0: 44;

          hence thesis by A86, Def10;

        end;

          suppose

           A87: p = { {A}} & q = { { {A}}} & u = { { {A}}};

          

          then ((f . (p,q)) "\/" (f . (q,u))) = (a "\/" (f . (q,u))) by Def10

          .= (( Bottom L) "\/" a) by A87, Def10

          .= a by WAYBEL_1: 3

          .= (f . (p,q)) by A87, Def10;

          hence thesis by A87;

        end;

          suppose

           A88: p = { { {A}}} & q = {A} & u = {A};

          

          then ((f . (p,q)) "\/" (f . (q,u))) = ((a "\/" b) "\/" (f . (q,u))) by Def10

          .= (( Bottom L) "\/" (a "\/" b)) by A88, Def10

          .= (a "\/" b) by WAYBEL_1: 3

          .= (f . (p,q)) by A88, Def10;

          hence thesis by A88;

        end;

          suppose

           A89: p = { { {A}}} & q = {A} & u = { {A}};

          then

           A90: (f . (p,u)) = a by Def10;

          ((f . (p,q)) "\/" (f . (q,u))) = ((a "\/" b) "\/" (f . (q,u))) by A89, Def10

          .= ((a "\/" b) "\/" b) by A89, Def10

          .= (a "\/" (b "\/" b)) by LATTICE3: 14

          .= (a "\/" b) by YELLOW_5: 1;

          hence thesis by A90, YELLOW_0: 22;

        end;

          suppose

           A91: p = { { {A}}} & q = {A} & u = { { {A}}};

          ( Bottom L) <= ((f . (p,q)) "\/" (f . (q,u))) by YELLOW_0: 44;

          hence thesis by A91, Def10;

        end;

          suppose

           A92: p = { { {A}}} & q = { {A}} & u = {A};

          

          then ((f . (p,q)) "\/" (f . (q,u))) = (a "\/" (f . (q,u))) by Def10

          .= (a "\/" b) by A92, Def10;

          hence thesis by A92, Def10;

        end;

          suppose

           A93: p = { { {A}}} & q = { {A}} & u = { {A}};

          

          then ((f . (p,q)) "\/" (f . (q,u))) = (a "\/" (f . (q,u))) by Def10

          .= (( Bottom L) "\/" a) by A93, Def10

          .= a by WAYBEL_1: 3

          .= (f . (p,q)) by A93, Def10;

          hence thesis by A93;

        end;

          suppose

           A94: p = { { {A}}} & q = { {A}} & u = { { {A}}};

          ( Bottom L) <= ((f . (p,q)) "\/" (f . (q,u))) by YELLOW_0: 44;

          hence thesis by A94, Def10;

        end;

          suppose

           A95: p = { { {A}}} & q = { { {A}}} & u = {A};

          

          then ((f . (p,q)) "\/" (f . (q,u))) = (( Bottom L) "\/" (f . (p,u))) by Def10

          .= (( Bottom L) "\/" (a "\/" b)) by A95, Def10

          .= (a "\/" b) by WAYBEL_1: 3;

          hence thesis by A95, Def10;

        end;

          suppose

           A96: p = { { {A}}} & q = { { {A}}} & u = { {A}};

          

          then ((f . (p,q)) "\/" (f . (q,u))) = (( Bottom L) "\/" (f . (p,u))) by Def10

          .= (( Bottom L) "\/" a) by A96, Def10

          .= a by WAYBEL_1: 3;

          hence thesis by A96, Def10;

        end;

          suppose

           A97: p = { { {A}}} & q = { { {A}}} & u = { { {A}}};

          ( Bottom L) <= ((f . (p,q)) "\/" (f . (q,u))) by YELLOW_0: 44;

          hence thesis by A97, Def10;

        end;

      end;

      

       A98: for p,q,u be Element of ( new_set A) st p in B & q in A & u in B holds (f . (p,u)) <= ((f . (p,q)) "\/" (f . (q,u)))

      proof

        let p,q,u be Element of ( new_set A);

        assume that

         A99: p in B and

         A100: q in A and

         A101: u in B;

        reconsider q9 = q as Element of A by A100;

        per cases by A99, A100, A101, ENUMSET1:def 1;

          suppose q in A & p = {A} & u = {A};

          then (f . (p,u)) = ( Bottom L) by Def10;

          hence thesis by YELLOW_0: 44;

        end;

          suppose

           A102: q in A & p = {A} & u = { {A}};

          

          then

           A103: ((f . (p,q)) "\/" (f . (q,u))) = ((f . (p,q)) "\/" (((d . (q9,x)) "\/" a) "\/" b)) by Def10

          .= ((f . (p,q)) "\/" ((d . (q9,x)) "\/" (a "\/" b))) by LATTICE3: 14

          .= (((f . (p,q)) "\/" (d . (q9,x))) "\/" (a "\/" b)) by LATTICE3: 14

          .= ((((f . (p,q)) "\/" (d . (q9,x))) "\/" a) "\/" b) by LATTICE3: 14;

          (f . (p,u)) = b by A102, Def10;

          hence thesis by A103, YELLOW_0: 22;

        end;

          suppose

           A104: q in A & p = {A} & u = { { {A}}};

          then

           A105: (f . (p,u)) = (a "\/" b) by Def10;

          ((f . (p,q)) "\/" (f . (q,u))) = (((d . (q9,x)) "\/" a) "\/" (f . (q,u))) by A104, Def10

          .= (((d . (q9,x)) "\/" a) "\/" ((d . (q9,y)) "\/" b)) by A104, Def10

          .= ((d . (q9,x)) "\/" (a "\/" ((d . (q9,y)) "\/" b))) by LATTICE3: 14

          .= ((d . (q9,x)) "\/" ((d . (q9,y)) "\/" (a "\/" b))) by LATTICE3: 14

          .= (((d . (q9,x)) "\/" (d . (q9,y))) "\/" (a "\/" b)) by LATTICE3: 14;

          hence thesis by A105, YELLOW_0: 22;

        end;

          suppose

           A106: q in A & p = { {A}} & u = {A};

          

          then

           A107: ((f . (p,q)) "\/" (f . (q,u))) = ((((d . (q9,x)) "\/" a) "\/" b) "\/" (f . (q,u))) by Def10

          .= ((f . (q,u)) "\/" ((d . (q9,x)) "\/" (a "\/" b))) by LATTICE3: 14

          .= (((f . (q,u)) "\/" (d . (q9,x))) "\/" (a "\/" b)) by LATTICE3: 14

          .= ((((f . (q,u)) "\/" (d . (q9,x))) "\/" a) "\/" b) by LATTICE3: 14;

          (f . (p,u)) = b by A106, Def10;

          hence thesis by A107, YELLOW_0: 22;

        end;

          suppose q in A & p = { {A}} & u = { {A}};

          then (f . (p,u)) = ( Bottom L) by Def10;

          hence thesis by YELLOW_0: 44;

        end;

          suppose

           A108: q in A & p = { {A}} & u = { { {A}}};

          

          then

           A109: ((f . (p,q)) "\/" (f . (q,u))) = ((((d . (q9,x)) "\/" a) "\/" b) "\/" (f . (q,u))) by Def10

          .= ((a "\/" ((d . (q9,x)) "\/" b)) "\/" (f . (q,u))) by LATTICE3: 14

          .= (a "\/" (((d . (q9,x)) "\/" b) "\/" (f . (q,u)))) by LATTICE3: 14;

          (f . (p,u)) = a by A108, Def10;

          hence thesis by A109, YELLOW_0: 22;

        end;

          suppose

           A110: q in A & p = { { {A}}} & u = {A};

          then

           A111: (f . (p,u)) = (a "\/" b) by Def10;

          ((f . (p,q)) "\/" (f . (q,u))) = (((d . (q9,y)) "\/" b) "\/" (f . (q,u))) by A110, Def10

          .= (((d . (q9,y)) "\/" b) "\/" ((d . (q9,x)) "\/" a)) by A110, Def10

          .= ((d . (q9,y)) "\/" (b "\/" ((d . (q9,x)) "\/" a))) by LATTICE3: 14

          .= ((d . (q9,y)) "\/" ((d . (q9,x)) "\/" (b "\/" a))) by LATTICE3: 14

          .= (((d . (q9,y)) "\/" (d . (q9,x))) "\/" (a "\/" b)) by LATTICE3: 14;

          hence thesis by A111, YELLOW_0: 22;

        end;

          suppose

           A112: q in A & p = { { {A}}} & u = { {A}};

          

          then

           A113: ((f . (p,q)) "\/" (f . (q,u))) = ((f . (p,q)) "\/" (((d . (q9,x)) "\/" a) "\/" b)) by Def10

          .= ((f . (p,q)) "\/" ((d . (q9,x)) "\/" (a "\/" b))) by LATTICE3: 14

          .= (((f . (p,q)) "\/" (d . (q9,x))) "\/" (a "\/" b)) by LATTICE3: 14

          .= ((((f . (p,q)) "\/" (d . (q9,x))) "\/" b) "\/" a) by LATTICE3: 14;

          (f . (p,u)) = a by A112, Def10;

          hence thesis by A113, YELLOW_0: 22;

        end;

          suppose q in A & p = { { {A}}} & u = { { {A}}};

          then (f . (p,u)) = ( Bottom L) by Def10;

          hence thesis by YELLOW_0: 44;

        end;

      end;

      

       A114: for p,q,u be Element of ( new_set A) st p in A & q in B & u in B holds (f . (p,u)) <= ((f . (p,q)) "\/" (f . (q,u)))

      proof

        let p,q,u be Element of ( new_set A);

        assume that

         A115: p in A and

         A116: q in B & u in B;

        reconsider p9 = p as Element of A by A115;

        per cases by A115, A116, ENUMSET1:def 1;

          suppose

           A117: p in A & q = {A} & u = {A};

          

          then ((f . (p,q)) "\/" (f . (q,u))) = (( Bottom L) "\/" (f . (p,q))) by Def10

          .= (f . (p,q)) by WAYBEL_1: 3;

          hence thesis by A117;

        end;

          suppose

           A118: p in A & q = {A} & u = { {A}};

          

          then (f . (p,u)) = (((d . (p9,x)) "\/" a) "\/" b) by Def10

          .= ((f . (p,q)) "\/" b) by A118, Def10;

          hence thesis by A118, Def10;

        end;

          suppose

           A119: p in A & q = {A} & u = { { {A}}};

          (d . (p9,y)) <= ((d . (p9,x)) "\/" (d . (x,y))) by A2;

          then ((d . (p9,y)) "\/" b) <= (((d . (p9,x)) "\/" (d . (x,y))) "\/" b) by WAYBEL_1: 2;

          then

           A120: (f . (p,u)) <= (((d . (p9,x)) "\/" (d . (x,y))) "\/" b) by A119, Def10;

          ((d . (p9,x)) "\/" b) <= ((d . (p9,x)) "\/" b);

          then (((d . (p9,x)) "\/" (d . (x,y))) "\/" b) = (((d . (p9,x)) "\/" b) "\/" (d . (x,y))) & (((d . (p9,x)) "\/" b) "\/" (d . (x,y))) <= (((d . (p9,x)) "\/" b) "\/" (a "\/" b)) by A14, LATTICE3: 14, YELLOW_3: 3;

          then

           A121: (f . (p,u)) <= (((d . (p9,x)) "\/" b) "\/" (a "\/" b)) by A120, ORDERS_2: 3;

          

           A122: (((d . (p9,x)) "\/" b) "\/" (a "\/" b)) = ((d . (p9,x)) "\/" ((b "\/" a) "\/" b)) by LATTICE3: 14

          .= ((d . (p9,x)) "\/" (a "\/" (b "\/" b))) by LATTICE3: 14

          .= ((d . (p9,x)) "\/" (a "\/" b)) by YELLOW_5: 1

          .= ((d . (p9,x)) "\/" ((a "\/" a) "\/" b)) by YELLOW_5: 1

          .= ((d . (p9,x)) "\/" (a "\/" (a "\/" b))) by LATTICE3: 14

          .= (((d . (p9,x)) "\/" a) "\/" (a "\/" b)) by LATTICE3: 14;

          (f . (p,q)) = ((d . (p9,x)) "\/" a) by A119, Def10;

          hence thesis by A119, A121, A122, Def10;

        end;

          suppose

           A123: p in A & q = { {A}} & u = {A};

          

          then (f . (p,q)) = (((d . (p9,x)) "\/" a) "\/" b) by Def10

          .= ((f . (p,u)) "\/" b) by A123, Def10;

          

          then ((f . (p,q)) "\/" (f . (q,u))) = (((f . (p,u)) "\/" b) "\/" b) by A123, Def10

          .= ((f . (p,u)) "\/" (b "\/" b)) by LATTICE3: 14

          .= ((f . (p,u)) "\/" b) by YELLOW_5: 1;

          hence thesis by YELLOW_0: 22;

        end;

          suppose

           A124: p in A & q = { {A}} & u = { {A}};

          

          then ((f . (p,q)) "\/" (f . (q,u))) = (( Bottom L) "\/" (f . (p,q))) by Def10

          .= (f . (p,q)) by WAYBEL_1: 3;

          hence thesis by A124;

        end;

          suppose

           A125: p in A & q = { {A}} & u = { { {A}}};

          (d . (p9,y)) <= ((d . (p9,x)) "\/" (d . (x,y))) by A2;

          then ((d . (p9,y)) "\/" b) <= (((d . (p9,x)) "\/" (d . (x,y))) "\/" b) by WAYBEL_1: 2;

          then

           A126: (f . (p,u)) <= (((d . (p9,x)) "\/" (d . (x,y))) "\/" b) by A125, Def10;

          ((d . (p9,x)) "\/" b) <= ((d . (p9,x)) "\/" b);

          then (((d . (p9,x)) "\/" (d . (x,y))) "\/" b) = (((d . (p9,x)) "\/" b) "\/" (d . (x,y))) & (((d . (p9,x)) "\/" b) "\/" (d . (x,y))) <= (((d . (p9,x)) "\/" b) "\/" (a "\/" b)) by A14, LATTICE3: 14, YELLOW_3: 3;

          then

           A127: (f . (p,u)) <= (((d . (p9,x)) "\/" b) "\/" (a "\/" b)) by A126, ORDERS_2: 3;

          

           A128: (((d . (p9,x)) "\/" b) "\/" (a "\/" b)) = ((d . (p9,x)) "\/" ((b "\/" a) "\/" b)) by LATTICE3: 14

          .= ((d . (p9,x)) "\/" (a "\/" (b "\/" b))) by LATTICE3: 14

          .= ((d . (p9,x)) "\/" (a "\/" b)) by YELLOW_5: 1

          .= ((d . (p9,x)) "\/" ((a "\/" a) "\/" b)) by YELLOW_5: 1

          .= ((d . (p9,x)) "\/" (a "\/" (a "\/" b))) by LATTICE3: 14

          .= (((d . (p9,x)) "\/" (a "\/" b)) "\/" a) by LATTICE3: 14

          .= ((((d . (p9,x)) "\/" a) "\/" b) "\/" a) by LATTICE3: 14;

          (f . (p,q)) = (((d . (p9,x)) "\/" a) "\/" b) by A125, Def10;

          hence thesis by A125, A127, A128, Def10;

        end;

          suppose

           A129: p in A & q = { { {A}}} & u = {A};

          (d . (p9,x)) <= ((d . (p9,y)) "\/" (d . (y,x))) by A2;

          then ((d . (p9,x)) "\/" a) <= (((d . (p9,y)) "\/" (d . (y,x))) "\/" a) by WAYBEL_1: 2;

          then

           A130: (f . (p,u)) <= (((d . (p9,y)) "\/" (d . (y,x))) "\/" a) by A129, Def10;

          (d . (y,x)) <= (a "\/" b) & ((d . (p9,y)) "\/" a) <= ((d . (p9,y)) "\/" a) by A1, A14;

          then (((d . (p9,y)) "\/" (d . (y,x))) "\/" a) = (((d . (p9,y)) "\/" a) "\/" (d . (y,x))) & (((d . (p9,y)) "\/" a) "\/" (d . (y,x))) <= (((d . (p9,y)) "\/" a) "\/" (a "\/" b)) by LATTICE3: 14, YELLOW_3: 3;

          then

           A131: (f . (p,u)) <= (((d . (p9,y)) "\/" a) "\/" (a "\/" b)) by A130, ORDERS_2: 3;

          

           A132: (((d . (p9,y)) "\/" a) "\/" (a "\/" b)) = ((((d . (p9,y)) "\/" a) "\/" a) "\/" b) by LATTICE3: 14

          .= (((d . (p9,y)) "\/" (a "\/" a)) "\/" b) by LATTICE3: 14

          .= (((d . (p9,y)) "\/" a) "\/" b) by YELLOW_5: 1

          .= ((d . (p9,y)) "\/" (a "\/" b)) by LATTICE3: 14

          .= ((d . (p9,y)) "\/" (a "\/" (b "\/" b))) by YELLOW_5: 1

          .= ((d . (p9,y)) "\/" ((a "\/" b) "\/" b)) by LATTICE3: 14

          .= (((d . (p9,y)) "\/" b) "\/" (a "\/" b)) by LATTICE3: 14;

          (f . (p,q)) = ((d . (p9,y)) "\/" b) by A129, Def10;

          hence thesis by A129, A131, A132, Def10;

        end;

          suppose

           A133: p in A & q = { { {A}}} & u = { {A}};

          (d . (p9,x)) <= ((d . (p9,y)) "\/" (d . (y,x))) by A2;

          then

           A134: ((d . (p9,x)) "\/" (a "\/" b)) <= (((d . (p9,y)) "\/" (d . (y,x))) "\/" (a "\/" b)) by WAYBEL_1: 2;

          (f . (p,u)) = (((d . (p9,x)) "\/" a) "\/" b) by A133, Def10;

          then

           A135: (f . (p,u)) <= (((d . (p9,y)) "\/" (d . (y,x))) "\/" (a "\/" b)) by A134, LATTICE3: 14;

          

           A136: (((d . (p9,y)) "\/" a) "\/" (a "\/" b)) = ((((d . (p9,y)) "\/" a) "\/" a) "\/" b) by LATTICE3: 14

          .= (((d . (p9,y)) "\/" (a "\/" a)) "\/" b) by LATTICE3: 14

          .= (((d . (p9,y)) "\/" a) "\/" b) by YELLOW_5: 1

          .= (((d . (p9,y)) "\/" b) "\/" a) by LATTICE3: 14;

          

           A137: (f . (p,q)) = ((d . (p9,y)) "\/" b) by A133, Def10;

          

           A138: ((d . (p9,y)) "\/" (a "\/" b)) <= ((d . (p9,y)) "\/" (a "\/" b));

          (d . (y,x)) <= (a "\/" b) & (((d . (p9,y)) "\/" (d . (y,x))) "\/" (a "\/" b)) = (((d . (p9,y)) "\/" (a "\/" b)) "\/" (d . (y,x))) by A1, A14, LATTICE3: 14;

          then

           A139: (((d . (p9,y)) "\/" (d . (y,x))) "\/" (a "\/" b)) <= (((d . (p9,y)) "\/" (a "\/" b)) "\/" (a "\/" b)) by A138, YELLOW_3: 3;

          (((d . (p9,y)) "\/" a) "\/" (a "\/" b)) = (((d . (p9,y)) "\/" a) "\/" ((a "\/" b) "\/" (a "\/" b))) by YELLOW_5: 1

          .= ((d . (p9,y)) "\/" (a "\/" ((a "\/" b) "\/" (a "\/" b)))) by LATTICE3: 14

          .= ((d . (p9,y)) "\/" ((a "\/" (a "\/" b)) "\/" (a "\/" b))) by LATTICE3: 14

          .= ((d . (p9,y)) "\/" (((a "\/" a) "\/" b) "\/" (a "\/" b))) by LATTICE3: 14

          .= ((d . (p9,y)) "\/" ((a "\/" b) "\/" (a "\/" b))) by YELLOW_5: 1

          .= (((d . (p9,y)) "\/" (a "\/" b)) "\/" (a "\/" b)) by LATTICE3: 14;

          then (f . (p,u)) <= (((d . (p9,y)) "\/" a) "\/" (a "\/" b)) by A139, A135, ORDERS_2: 3;

          hence thesis by A133, A137, A136, Def10;

        end;

          suppose

           A140: p in A & q = { { {A}}} & u = { { {A}}};

          

          then ((f . (p,q)) "\/" (f . (q,u))) = (( Bottom L) "\/" (f . (p,q))) by Def10

          .= (f . (p,q)) by WAYBEL_1: 3;

          hence thesis by A140;

        end;

      end;

      

       A141: for p,q,u be Element of ( new_set A) st p in A & q in A & u in A holds (f . (p,u)) <= ((f . (p,q)) "\/" (f . (q,u)))

      proof

        let p,q,u be Element of ( new_set A);

        assume p in A & q in A & u in A;

        then

        reconsider p9 = p, q9 = q, u9 = u as Element of A;

        

         A142: (f . (q,u)) = (d . (q9,u9)) by Def10;

        (f . (p,u)) = (d . (p9,u9)) & (f . (p,q)) = (d . (p9,q9)) by Def10;

        hence thesis by A2, A142;

      end;

      for p,q,u be Element of ( new_set A) holds (f . (p,u)) <= ((f . (p,q)) "\/" (f . (q,u)))

      proof

        let p,q,u be Element of ( new_set A);

        per cases by XBOOLE_0:def 3;

          suppose p in A & q in A & u in A;

          hence thesis by A141;

        end;

          suppose p in A & q in A & u in B;

          hence thesis by A54;

        end;

          suppose p in A & q in B & u in A;

          hence thesis by A3;

        end;

          suppose p in A & q in B & u in B;

          hence thesis by A114;

        end;

          suppose p in B & q in A & u in A;

          hence thesis by A42;

        end;

          suppose p in B & q in A & u in B;

          hence thesis by A98;

        end;

          suppose p in B & q in B & u in A;

          hence thesis by A15;

        end;

          suppose p in B & q in B & u in B;

          hence thesis by A65;

        end;

      end;

      hence thesis;

    end;

    theorem :: LATTICE5:19

    

     Th19: for d be BiFunction of A, L holds for q be Element of [:A, A, the carrier of L, the carrier of L:] holds d c= ( new_bi_fun (d,q))

    proof

      let d be BiFunction of A, L;

      let q be Element of [:A, A, the carrier of L, the carrier of L:];

      set g = ( new_bi_fun (d,q));

      

       A1: A c= ( new_set A) by XBOOLE_1: 7;

      

       A2: for z be object st z in ( dom d) holds (d . z) = (g . z)

      proof

        let z be object;

        assume

         A3: z in ( dom d);

        then

        consider x,y be object such that

         A4: [x, y] = z by RELAT_1:def 1;

        reconsider x9 = x, y9 = y as Element of A by A3, A4, ZFMISC_1: 87;

        (d . [x, y]) = (d . (x9,y9))

        .= (g . (x9,y9)) by Def10

        .= (g . [x, y]);

        hence thesis by A4;

      end;

      ( dom d) = [:A, A:] & ( dom g) = [:( new_set A), ( new_set A):] by FUNCT_2:def 1;

      then ( dom d) c= ( dom g) by A1, ZFMISC_1: 96;

      hence thesis by A2, GRFUNC_1: 2;

    end;

    definition

      let A, L;

      let d be BiFunction of A, L;

      :: LATTICE5:def11

      func DistEsti (d) -> Cardinal means

      : Def11: (it ,{ [x, y, a, b] where x be Element of A, y be Element of A, a be Element of L, b be Element of L : (d . (x,y)) <= (a "\/" b) }) are_equipotent ;

      existence

      proof

        set D = { [x, y, a, b] where x be Element of A, y be Element of A, a be Element of L, b be Element of L : (d . (x,y)) <= (a "\/" b) };

        take ( card D);

        thus thesis by CARD_1:def 2;

      end;

      uniqueness by WELLORD2: 15, CARD_1: 2;

    end

    theorem :: LATTICE5:20

    

     Th20: for d be distance_function of A, L holds ( DistEsti d) <> {}

    proof

      let d be distance_function of A, L;

      set X = { [x, y, a, b] where x be Element of A, y be Element of A, a be Element of L, b be Element of L : (d . (x,y)) <= (a "\/" b) };

      set x9 = the Element of A;

      consider z be set such that

       A1: z = [x9, x9, ( Bottom L), ( Bottom L)];

      

       A2: (( DistEsti d),X) are_equipotent by Def11;

      (d . (x9,x9)) = ( Bottom L) by Def6

      .= (( Bottom L) "\/" ( Bottom L)) by YELLOW_5: 1;

      then z in X by A1;

      hence thesis by A2, CARD_1: 26;

    end;

    reserve T,L1 for Sequence,

O,O1,O2,O3,C for Ordinal;

    definition

      let A;

      let O;

      :: LATTICE5:def12

      func ConsecutiveSet (A,O) -> set means

      : Def12: ex L0 be Sequence st it = ( last L0) & ( dom L0) = ( succ O) & (L0 . 0 ) = A & (for C be Ordinal st ( succ C) in ( succ O) holds (L0 . ( succ C)) = ( new_set (L0 . C))) & for C be Ordinal st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L0 . C) = ( union ( rng (L0 | C)));

      correctness

      proof

        deffunc D( Ordinal, Sequence) = ( union ( rng $2));

        deffunc C( Ordinal, set) = ( new_set $2);

        (ex x be object, L1 st x = ( last L1) & ( dom L1) = ( succ O) & (L1 . 0 ) = A & (for C be Ordinal st ( succ C) in ( succ O) holds (L1 . ( succ C)) = C(C,.)) & for C be Ordinal st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L1 . C) = D(C,|)) & for x1,x2 be set st (ex L1 st x1 = ( last L1) & ( dom L1) = ( succ O) & (L1 . 0 ) = A & (for C st ( succ C) in ( succ O) holds (L1 . ( succ C)) = C(C,.)) & for C st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L1 . C) = D(C,|)) & (ex L1 st x2 = ( last L1) & ( dom L1) = ( succ O) & (L1 . 0 ) = A & (for C st ( succ C) in ( succ O) holds (L1 . ( succ C)) = C(C,.)) & for C st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L1 . C) = D(C,|)) holds x1 = x2 from ORDINAL2:sch 7;

        hence thesis;

      end;

    end

    theorem :: LATTICE5:21

    

     Th21: ( ConsecutiveSet (A, 0 )) = A

    proof

      deffunc V( Ordinal, Sequence) = ( union ( rng $2));

      deffunc U( Ordinal, set) = ( new_set $2);

      deffunc F( Ordinal) = ( ConsecutiveSet (A,$1));

      

       A1: for O be Ordinal, x be object holds x = F(O) iff ex L0 be Sequence st x = ( last L0) & ( dom L0) = ( succ O) & (L0 . 0 ) = A & (for C be Ordinal st ( succ C) in ( succ O) holds (L0 . ( succ C)) = U(C,.)) & for C be Ordinal st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L0 . C) = V(C,|) by Def12;

      thus F(0) = A from ORDINAL2:sch 8( A1);

    end;

    theorem :: LATTICE5:22

    

     Th22: ( ConsecutiveSet (A,( succ O))) = ( new_set ( ConsecutiveSet (A,O)))

    proof

      deffunc V( Ordinal, Sequence) = ( union ( rng $2));

      deffunc U( Ordinal, set) = ( new_set $2);

      deffunc F( Ordinal) = ( ConsecutiveSet (A,$1));

      

       A1: for O be Ordinal, It be object holds It = F(O) iff ex L0 be Sequence st It = ( last L0) & ( dom L0) = ( succ O) & (L0 . 0 ) = A & (for C be Ordinal st ( succ C) in ( succ O) holds (L0 . ( succ C)) = U(C,.)) & for C be Ordinal st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L0 . C) = V(C,|) by Def12;

      for O holds F(succ) = U(O,F) from ORDINAL2:sch 9( A1);

      hence thesis;

    end;

    theorem :: LATTICE5:23

    

     Th23: O <> 0 & O is limit_ordinal & ( dom T) = O & (for O1 be Ordinal st O1 in O holds (T . O1) = ( ConsecutiveSet (A,O1))) implies ( ConsecutiveSet (A,O)) = ( union ( rng T))

    proof

      deffunc V( Ordinal, Sequence) = ( union ( rng $2));

      deffunc U( Ordinal, set) = ( new_set $2);

      deffunc F( Ordinal) = ( ConsecutiveSet (A,$1));

      assume that

       A1: O <> 0 & O is limit_ordinal and

       A2: ( dom T) = O and

       A3: for O1 be Ordinal st O1 in O holds (T . O1) = F(O1);

      

       A4: for O be Ordinal, x be object holds x = F(O) iff ex L0 be Sequence st x = ( last L0) & ( dom L0) = ( succ O) & (L0 . 0 ) = A & (for C be Ordinal st ( succ C) in ( succ O) holds (L0 . ( succ C)) = U(C,.)) & for C be Ordinal st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L0 . C) = V(C,|) by Def12;

      thus F(O) = V(O,T) from ORDINAL2:sch 10( A4, A1, A2, A3);

    end;

    registration

      let A;

      let O;

      cluster ( ConsecutiveSet (A,O)) -> non empty;

      coherence

      proof

        defpred X[ Ordinal] means ( ConsecutiveSet (A,$1)) is non empty;

        

         A1: for O st X[O] holds X[( succ O)]

        proof

          let O1;

          assume ( ConsecutiveSet (A,O1)) is non empty;

          ( ConsecutiveSet (A,( succ O1))) = ( new_set ( ConsecutiveSet (A,O1))) by Th22;

          hence thesis;

        end;

        

         A2: for O st O <> 0 & O is limit_ordinal & for B be Ordinal st B in O holds X[B] holds X[O]

        proof

          deffunc U( Ordinal) = ( ConsecutiveSet (A,$1));

          let O1;

          assume that

           A3: O1 <> 0 and

           A4: O1 is limit_ordinal and for O2 st O2 in O1 holds ( ConsecutiveSet (A,O2)) is non empty;

          

           A5: {} in O1 by A3, ORDINAL3: 8;

          consider Ls be Sequence such that

           A6: ( dom Ls) = O1 & for O2 be Ordinal st O2 in O1 holds (Ls . O2) = U(O2) from ORDINAL2:sch 2;

          (Ls . {} ) = ( ConsecutiveSet (A, {} )) by A3, A6, ORDINAL3: 8

          .= A by Th21;

          then

           A7: A in ( rng Ls) by A6, A5, FUNCT_1:def 3;

          ( ConsecutiveSet (A,O1)) = ( union ( rng Ls)) by A3, A4, A6, Th23;

          then A c= ( ConsecutiveSet (A,O1)) by A7, ZFMISC_1: 74;

          hence thesis;

        end;

        

         A8: X[ 0 ] by Th21;

        for O holds X[O] from ORDINAL2:sch 1( A8, A1, A2);

        hence thesis;

      end;

    end

    theorem :: LATTICE5:24

    

     Th24: A c= ( ConsecutiveSet (A,O))

    proof

      defpred X[ Ordinal] means A c= ( ConsecutiveSet (A,$1));

      

       A1: for O1 st X[O1] holds X[( succ O1)]

      proof

        let O1;

        ( ConsecutiveSet (A,( succ O1))) = ( new_set ( ConsecutiveSet (A,O1))) by Th22;

        then

         A2: ( ConsecutiveSet (A,O1)) c= ( ConsecutiveSet (A,( succ O1))) by XBOOLE_1: 7;

        assume A c= ( ConsecutiveSet (A,O1));

        hence thesis by A2, XBOOLE_1: 1;

      end;

      

       A3: for O2 st O2 <> 0 & O2 is limit_ordinal & for O1 st O1 in O2 holds X[O1] holds X[O2]

      proof

        deffunc U( Ordinal) = ( ConsecutiveSet (A,$1));

        let O2;

        assume that

         A4: O2 <> 0 and

         A5: O2 is limit_ordinal and for O1 st O1 in O2 holds A c= ( ConsecutiveSet (A,O1));

        

         A6: {} in O2 by A4, ORDINAL3: 8;

        consider Ls be Sequence such that

         A7: ( dom Ls) = O2 & for O1 be Ordinal st O1 in O2 holds (Ls . O1) = U(O1) from ORDINAL2:sch 2;

        (Ls . {} ) = ( ConsecutiveSet (A, {} )) by A4, A7, ORDINAL3: 8

        .= A by Th21;

        then

         A8: A in ( rng Ls) by A7, A6, FUNCT_1:def 3;

        ( ConsecutiveSet (A,O2)) = ( union ( rng Ls)) by A4, A5, A7, Th23;

        hence thesis by A8, ZFMISC_1: 74;

      end;

      

       A9: X[ 0 ] by Th21;

      for O holds X[O] from ORDINAL2:sch 1( A9, A1, A3);

      hence thesis;

    end;

    definition

      let A, L;

      let d be BiFunction of A, L;

      :: LATTICE5:def13

      mode QuadrSeq of d -> Sequence of [:A, A, the carrier of L, the carrier of L:] means

      : Def13: ( dom it ) is Cardinal & it is one-to-one & ( rng it ) = { [x, y, a, b] where x be Element of A, y be Element of A, a be Element of L, b be Element of L : (d . (x,y)) <= (a "\/" b) };

      existence

      proof

        set X = { [x, y, a, b] where x be Element of A, y be Element of A, a be Element of L, b be Element of L : (d . (x,y)) <= (a "\/" b) };

        (( card X),X) are_equipotent by CARD_1:def 2;

        then

        consider f be Function such that

         A1: f is one-to-one and

         A2: ( dom f) = ( card X) and

         A3: ( rng f) = X by WELLORD2:def 4;

        reconsider f as Sequence by A2, ORDINAL1:def 7;

        ( rng f) c= [:A, A, the carrier of L, the carrier of L:]

        proof

          let z be object;

          assume z in ( rng f);

          then ex x,y be Element of A, a,b be Element of L st z = [x, y, a, b] & (d . (x,y)) <= (a "\/" b) by A3;

          hence thesis;

        end;

        then

        reconsider f as Sequence of [:A, A, the carrier of L, the carrier of L:] by RELAT_1:def 19;

        take f;

        thus ( dom f) is Cardinal by A2;

        thus f is one-to-one by A1;

        thus thesis by A3;

      end;

    end

    definition

      let A, L;

      let d be BiFunction of A, L;

      let q be QuadrSeq of d;

      let O;

      assume

       A1: O in ( dom q);

      :: LATTICE5:def14

      func Quadr (q,O) -> Element of [:( ConsecutiveSet (A,O)), ( ConsecutiveSet (A,O)), the carrier of L, the carrier of L:] equals

      : Def14: (q . O);

      correctness

      proof

        (q . O) in ( rng q) by A1, FUNCT_1:def 3;

        then (q . O) in { [x, y, a, b] where x be Element of A, y be Element of A, a be Element of L, b be Element of L : (d . (x,y)) <= (a "\/" b) } by Def13;

        then

        consider x,y be Element of A, a,b be Element of L such that

         A2: (q . O) = [x, y, a, b] and (d . (x,y)) <= (a "\/" b);

        reconsider a, b as Element of L;

        A c= ( ConsecutiveSet (A,O)) by Th24;

        then

        reconsider x, y as Element of ( ConsecutiveSet (A,O));

        reconsider z = [x, y, a, b] as Element of [:( ConsecutiveSet (A,O)), ( ConsecutiveSet (A,O)), the carrier of L, the carrier of L:];

        z = (q . O) by A2;

        hence thesis;

      end;

    end

    theorem :: LATTICE5:25

    

     Th25: for d be BiFunction of A, L, q be QuadrSeq of d holds O in ( DistEsti d) iff O in ( dom q)

    proof

      let d be BiFunction of A, L;

      let q be QuadrSeq of d;

      reconsider N = ( dom q) as Cardinal by Def13;

      reconsider M = ( DistEsti d) as Cardinal;

      q is one-to-one by Def13;

      then

       A1: (( dom q),( rng q)) are_equipotent by WELLORD2:def 4;

      (( DistEsti d),{ [x, y, a, b] where x be Element of A, y be Element of A, a be Element of L, b be Element of L : (d . (x,y)) <= (a "\/" b) }) are_equipotent by Def11;

      then (( DistEsti d),( rng q)) are_equipotent by Def13;

      then (( DistEsti d),( dom q)) are_equipotent by A1, WELLORD2: 15;

      then

       A2: M = N by CARD_1: 2;

      hence O in ( DistEsti d) implies O in ( dom q);

      assume O in ( dom q);

      hence thesis by A2;

    end;

    definition

      let A, L;

      let z be set;

      assume

       A1: z is BiFunction of A, L;

      :: LATTICE5:def15

      func BiFun (z,A,L) -> BiFunction of A, L equals

      : Def15: z;

      coherence by A1;

    end

    definition

      let A, L;

      let d be BiFunction of A, L;

      let q be QuadrSeq of d;

      let O;

      :: LATTICE5:def16

      func ConsecutiveDelta (q,O) -> set means

      : Def16: ex L0 be Sequence st it = ( last L0) & ( dom L0) = ( succ O) & (L0 . 0 ) = d & (for C be Ordinal st ( succ C) in ( succ O) holds (L0 . ( succ C)) = ( new_bi_fun (( BiFun ((L0 . C),( ConsecutiveSet (A,C)),L)),( Quadr (q,C))))) & for C be Ordinal st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L0 . C) = ( union ( rng (L0 | C)));

      correctness

      proof

        deffunc D( Ordinal, Sequence) = ( union ( rng $2));

        deffunc C( Ordinal, set) = ( new_bi_fun (( BiFun ($2,( ConsecutiveSet (A,$1)),L)),( Quadr (q,$1))));

        (ex x be object, L1 st x = ( last L1) & ( dom L1) = ( succ O) & (L1 . 0 ) = d & (for C be Ordinal st ( succ C) in ( succ O) holds (L1 . ( succ C)) = C(C,.)) & for C be Ordinal st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L1 . C) = D(C,|)) & for x1,x2 be set st (ex L1 st x1 = ( last L1) & ( dom L1) = ( succ O) & (L1 . 0 ) = d & (for C st ( succ C) in ( succ O) holds (L1 . ( succ C)) = C(C,.)) & for C st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L1 . C) = D(C,|)) & (ex L1 st x2 = ( last L1) & ( dom L1) = ( succ O) & (L1 . 0 ) = d & (for C st ( succ C) in ( succ O) holds (L1 . ( succ C)) = C(C,.)) & for C st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L1 . C) = D(C,|)) holds x1 = x2 from ORDINAL2:sch 7;

        hence thesis;

      end;

    end

    theorem :: LATTICE5:26

    

     Th26: for d be BiFunction of A, L holds for q be QuadrSeq of d holds ( ConsecutiveDelta (q, 0 )) = d

    proof

      deffunc D( Ordinal, Sequence) = ( union ( rng $2));

      let d be BiFunction of A, L, q be QuadrSeq of d;

      deffunc C( Ordinal, set) = ( new_bi_fun (( BiFun ($2,( ConsecutiveSet (A,$1)),L)),( Quadr (q,$1))));

      deffunc F( Ordinal) = ( ConsecutiveDelta (q,$1));

      

       A1: for O be Ordinal, It be object holds It = F(O) iff ex L0 be Sequence st It = ( last L0) & ( dom L0) = ( succ O) & (L0 . 0 ) = d & (for C be Ordinal st ( succ C) in ( succ O) holds (L0 . ( succ C)) = C(C,.)) & for C be Ordinal st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L0 . C) = D(C,|) by Def16;

      thus F(0) = d from ORDINAL2:sch 8( A1);

    end;

    theorem :: LATTICE5:27

    

     Th27: for d be BiFunction of A, L holds for q be QuadrSeq of d holds ( ConsecutiveDelta (q,( succ O))) = ( new_bi_fun (( BiFun (( ConsecutiveDelta (q,O)),( ConsecutiveSet (A,O)),L)),( Quadr (q,O))))

    proof

      deffunc D( Ordinal, Sequence) = ( union ( rng $2));

      let d be BiFunction of A, L;

      let q be QuadrSeq of d;

      deffunc C( Ordinal, set) = ( new_bi_fun (( BiFun ($2,( ConsecutiveSet (A,$1)),L)),( Quadr (q,$1))));

      deffunc F( Ordinal) = ( ConsecutiveDelta (q,$1));

      

       A1: for O be Ordinal, It be object holds It = F(O) iff ex L0 be Sequence st It = ( last L0) & ( dom L0) = ( succ O) & (L0 . 0 ) = d & (for C be Ordinal st ( succ C) in ( succ O) holds (L0 . ( succ C)) = C(C,.)) & for C be Ordinal st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L0 . C) = D(C,|) by Def16;

      for O holds F(succ) = C(O,F) from ORDINAL2:sch 9( A1);

      hence thesis;

    end;

    theorem :: LATTICE5:28

    

     Th28: for d be BiFunction of A, L holds for q be QuadrSeq of d holds O <> 0 & O is limit_ordinal & ( dom T) = O & (for O1 be Ordinal st O1 in O holds (T . O1) = ( ConsecutiveDelta (q,O1))) implies ( ConsecutiveDelta (q,O)) = ( union ( rng T))

    proof

      deffunc D( Ordinal, Sequence) = ( union ( rng $2));

      let d be BiFunction of A, L;

      let q be QuadrSeq of d;

      deffunc C( Ordinal, set) = ( new_bi_fun (( BiFun ($2,( ConsecutiveSet (A,$1)),L)),( Quadr (q,$1))));

      deffunc F( Ordinal) = ( ConsecutiveDelta (q,$1));

      assume that

       A1: O <> 0 & O is limit_ordinal and

       A2: ( dom T) = O and

       A3: for O1 be Ordinal st O1 in O holds (T . O1) = F(O1);

      

       A4: for O be Ordinal, It be object holds It = F(O) iff ex L0 be Sequence st It = ( last L0) & ( dom L0) = ( succ O) & (L0 . 0 ) = d & (for C be Ordinal st ( succ C) in ( succ O) holds (L0 . ( succ C)) = C(C,.)) & for C be Ordinal st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L0 . C) = D(C,|) by Def16;

      thus F(O) = D(O,T) from ORDINAL2:sch 10( A4, A1, A2, A3);

    end;

    theorem :: LATTICE5:29

    

     Th29: O1 c= O2 implies ( ConsecutiveSet (A,O1)) c= ( ConsecutiveSet (A,O2))

    proof

      defpred X[ Ordinal] means O1 c= $1 implies ( ConsecutiveSet (A,O1)) c= ( ConsecutiveSet (A,$1));

      

       A1: for O2 st X[O2] holds X[( succ O2)]

      proof

        let O2;

        assume

         A2: O1 c= O2 implies ( ConsecutiveSet (A,O1)) c= ( ConsecutiveSet (A,O2));

        assume

         A3: O1 c= ( succ O2);

        per cases ;

          suppose O1 = ( succ O2);

          hence thesis;

        end;

          suppose O1 <> ( succ O2);

          then O1 c< ( succ O2) by A3;

          then

           A4: O1 in ( succ O2) by ORDINAL1: 11;

          ( ConsecutiveSet (A,O2)) c= ( new_set ( ConsecutiveSet (A,O2))) by XBOOLE_1: 7;

          then ( ConsecutiveSet (A,O1)) c= ( new_set ( ConsecutiveSet (A,O2))) by A2, A4, ORDINAL1: 22;

          hence thesis by Th22;

        end;

      end;

      

       A5: for O2 st O2 <> 0 & O2 is limit_ordinal & for O3 st O3 in O2 holds X[O3] holds X[O2]

      proof

        deffunc U( Ordinal) = ( ConsecutiveSet (A,$1));

        let O2;

        assume that

         A6: O2 <> 0 & O2 is limit_ordinal and for O3 st O3 in O2 holds O1 c= O3 implies ( ConsecutiveSet (A,O1)) c= ( ConsecutiveSet (A,O3));

        consider L be Sequence such that

         A7: ( dom L) = O2 & for O3 be Ordinal st O3 in O2 holds (L . O3) = U(O3) from ORDINAL2:sch 2;

        

         A8: ( ConsecutiveSet (A,O2)) = ( union ( rng L)) by A6, A7, Th23;

        assume

         A9: O1 c= O2;

        per cases ;

          suppose O1 = O2;

          hence thesis;

        end;

          suppose O1 <> O2;

          then

           A10: O1 c< O2 by A9;

          then O1 in O2 by ORDINAL1: 11;

          then

           A11: (L . O1) in ( rng L) by A7, FUNCT_1:def 3;

          (L . O1) = ( ConsecutiveSet (A,O1)) by A7, A10, ORDINAL1: 11;

          hence thesis by A8, A11, ZFMISC_1: 74;

        end;

      end;

      

       A12: X[ 0 ];

      for O2 holds X[O2] from ORDINAL2:sch 1( A12, A1, A5);

      hence thesis;

    end;

    theorem :: LATTICE5:30

    

     Th30: for d be BiFunction of A, L holds for q be QuadrSeq of d holds ( ConsecutiveDelta (q,O)) is BiFunction of ( ConsecutiveSet (A,O)), L

    proof

      let d be BiFunction of A, L;

      let q be QuadrSeq of d;

      defpred Y[ Ordinal] means ( ConsecutiveDelta (q,$1)) is BiFunction of ( ConsecutiveSet (A,$1)), L;

      

       A1: for O1 st Y[O1] holds Y[( succ O1)]

      proof

        let O1;

        assume ( ConsecutiveDelta (q,O1)) is BiFunction of ( ConsecutiveSet (A,O1)), L;

        then

        reconsider CD = ( ConsecutiveDelta (q,O1)) as BiFunction of ( ConsecutiveSet (A,O1)), L;

        

         A2: ( ConsecutiveSet (A,( succ O1))) = ( new_set ( ConsecutiveSet (A,O1))) by Th22;

        ( ConsecutiveDelta (q,( succ O1))) = ( new_bi_fun (( BiFun (( ConsecutiveDelta (q,O1)),( ConsecutiveSet (A,O1)),L)),( Quadr (q,O1)))) by Th27

        .= ( new_bi_fun (CD,( Quadr (q,O1)))) by Def15;

        hence thesis by A2;

      end;

      

       A3: for O1 st O1 <> 0 & O1 is limit_ordinal & for O2 st O2 in O1 holds Y[O2] holds Y[O1]

      proof

        deffunc U( Ordinal) = ( ConsecutiveDelta (q,$1));

        let O1;

        assume that

         A4: O1 <> 0 and

         A5: O1 is limit_ordinal and

         A6: for O2 st O2 in O1 holds ( ConsecutiveDelta (q,O2)) is BiFunction of ( ConsecutiveSet (A,O2)), L;

        consider Ls be Sequence such that

         A7: ( dom Ls) = O1 & for O2 be Ordinal st O2 in O1 holds (Ls . O2) = U(O2) from ORDINAL2:sch 2;

        

         A8: for O, O2 st O c= O2 & O2 in ( dom Ls) holds (Ls . O) c= (Ls . O2)

        proof

          let O;

          defpred X[ Ordinal] means O c= $1 & $1 in ( dom Ls) implies (Ls . O) c= (Ls . $1);

          

           A9: for O2 st O2 <> 0 & O2 is limit_ordinal & for O3 st O3 in O2 holds X[O3] holds X[O2]

          proof

            deffunc U( Ordinal) = ( ConsecutiveDelta (q,$1));

            let O2;

            assume that

             A10: O2 <> 0 & O2 is limit_ordinal and for O3 st O3 in O2 holds O c= O3 & O3 in ( dom Ls) implies (Ls . O) c= (Ls . O3);

            assume that

             A11: O c= O2 and

             A12: O2 in ( dom Ls);

            consider Lt be Sequence such that

             A13: ( dom Lt) = O2 & for O3 be Ordinal st O3 in O2 holds (Lt . O3) = U(O3) from ORDINAL2:sch 2;

            

             A14: (Ls . O2) = ( ConsecutiveDelta (q,O2)) by A7, A12

            .= ( union ( rng Lt)) by A10, A13, Th28;

            per cases ;

              suppose O = O2;

              hence thesis;

            end;

              suppose O <> O2;

              then

               A15: O c< O2 by A11;

              then

               A16: O in O2 by ORDINAL1: 11;

              

              then (Ls . O) = ( ConsecutiveDelta (q,O)) by A7, A12, ORDINAL1: 10

              .= (Lt . O) by A13, A15, ORDINAL1: 11;

              then (Ls . O) in ( rng Lt) by A13, A16, FUNCT_1:def 3;

              hence thesis by A14, ZFMISC_1: 74;

            end;

          end;

          

           A17: for O2 st X[O2] holds X[( succ O2)]

          proof

            let O2;

            assume

             A18: O c= O2 & O2 in ( dom Ls) implies (Ls . O) c= (Ls . O2);

            assume that

             A19: O c= ( succ O2) and

             A20: ( succ O2) in ( dom Ls);

            per cases ;

              suppose O = ( succ O2);

              hence thesis;

            end;

              suppose O <> ( succ O2);

              then O c< ( succ O2) by A19;

              then

               A21: O in ( succ O2) by ORDINAL1: 11;

              

               A22: O2 in ( succ O2) by ORDINAL1: 6;

              then O2 in ( dom Ls) by A20, ORDINAL1: 10;

              then

              reconsider cd2 = ( ConsecutiveDelta (q,O2)) as BiFunction of ( ConsecutiveSet (A,O2)), L by A6, A7;

              (Ls . ( succ O2)) = ( ConsecutiveDelta (q,( succ O2))) by A7, A20

              .= ( new_bi_fun (( BiFun (( ConsecutiveDelta (q,O2)),( ConsecutiveSet (A,O2)),L)),( Quadr (q,O2)))) by Th27

              .= ( new_bi_fun (cd2,( Quadr (q,O2)))) by Def15;

              then ( ConsecutiveDelta (q,O2)) c= (Ls . ( succ O2)) by Th19;

              then (Ls . O2) c= (Ls . ( succ O2)) by A7, A20, A22, ORDINAL1: 10;

              hence thesis by A18, A20, A21, A22, ORDINAL1: 10, ORDINAL1: 22;

            end;

          end;

          

           A23: X[ 0 ];

          thus for O2 holds X[O2] from ORDINAL2:sch 1( A23, A17, A9);

        end;

        for x,y be set st x in ( rng Ls) & y in ( rng Ls) holds (x,y) are_c=-comparable

        proof

          let x,y be set;

          assume that

           A24: x in ( rng Ls) and

           A25: y in ( rng Ls);

          consider o1 be object such that

           A26: o1 in ( dom Ls) and

           A27: (Ls . o1) = x by A24, FUNCT_1:def 3;

          consider o2 be object such that

           A28: o2 in ( dom Ls) and

           A29: (Ls . o2) = y by A25, FUNCT_1:def 3;

          reconsider o19 = o1, o29 = o2 as Ordinal by A26, A28;

          o19 c= o29 or o29 c= o19;

          then x c= y or y c= x by A8, A26, A27, A28, A29;

          hence thesis;

        end;

        then

         A30: ( rng Ls) is c=-linear;

        set Y = the carrier of L, X = [:( ConsecutiveSet (A,O1)), ( ConsecutiveSet (A,O1)):], f = ( union ( rng Ls));

        ( rng Ls) c= ( PFuncs (X,Y))

        proof

          let z be object;

          assume z in ( rng Ls);

          then

          consider o be object such that

           A31: o in ( dom Ls) and

           A32: z = (Ls . o) by FUNCT_1:def 3;

          reconsider o as Ordinal by A31;

          (Ls . o) = ( ConsecutiveDelta (q,o)) by A7, A31;

          then

          reconsider h = (Ls . o) as BiFunction of ( ConsecutiveSet (A,o)), L by A6, A7, A31;

          o c= O1 by A7, A31, ORDINAL1:def 2;

          then ( dom h) = [:( ConsecutiveSet (A,o)), ( ConsecutiveSet (A,o)):] & ( ConsecutiveSet (A,o)) c= ( ConsecutiveSet (A,O1)) by Th29, FUNCT_2:def 1;

          then ( rng h) c= Y & ( dom h) c= X by ZFMISC_1: 96;

          hence thesis by A32, PARTFUN1:def 3;

        end;

        then f in ( PFuncs (X,Y)) by A30, TREES_2: 40;

        then

         A33: ex g be Function st f = g & ( dom g) c= X & ( rng g) c= Y by PARTFUN1:def 3;

        reconsider o1 = O1 as non empty Ordinal by A4;

        set YY = the set of all [:( ConsecutiveSet (A,O2)), ( ConsecutiveSet (A,O2)):] where O2 be Element of o1;

        deffunc U( Ordinal) = ( ConsecutiveSet (A,$1));

        consider Ts be Sequence such that

         A34: ( dom Ts) = O1 & for O2 be Ordinal st O2 in O1 holds (Ts . O2) = U(O2) from ORDINAL2:sch 2;

        Ls is Function-yielding

        proof

          let x be object;

          assume

           A35: x in ( dom Ls);

          then

          reconsider o = x as Ordinal;

          (Ls . o) = ( ConsecutiveDelta (q,o)) by A7, A35;

          hence thesis by A6, A7, A35;

        end;

        then

        reconsider LsF = Ls as Function-yielding Function;

        

         A36: ( rng ( doms LsF)) = YY

        proof

          thus ( rng ( doms LsF)) c= YY

          proof

            let Z be object;

            assume Z in ( rng ( doms LsF));

            then

            consider o be object such that

             A37: o in ( dom ( doms LsF)) and

             A38: Z = (( doms LsF) . o) by FUNCT_1:def 3;

            

             A39: o in ( dom LsF) by A37, FUNCT_6: 59;

            then

            reconsider o9 = o as Element of o1 by A7;

            (Ls . o9) = ( ConsecutiveDelta (q,o9)) by A7;

            then

            reconsider ls = (Ls . o9) as BiFunction of ( ConsecutiveSet (A,o9)), L by A6;

            Z = ( dom ls) by A38, A39, FUNCT_6: 22

            .= [:( ConsecutiveSet (A,o9)), ( ConsecutiveSet (A,o9)):] by FUNCT_2:def 1;

            hence thesis;

          end;

          let Z be object;

          assume Z in YY;

          then

          consider o be Element of o1 such that

           A40: Z = [:( ConsecutiveSet (A,o)), ( ConsecutiveSet (A,o)):];

          (Ls . o) = ( ConsecutiveDelta (q,o)) by A7;

          then

          reconsider ls = (Ls . o) as BiFunction of ( ConsecutiveSet (A,o)), L by A6;

          o in ( dom LsF) by A7;

          then

           A41: o in ( dom ( doms LsF)) by FUNCT_6: 59;

          Z = ( dom ls) by A40, FUNCT_2:def 1

          .= (( doms LsF) . o) by A7, FUNCT_6: 22;

          hence thesis by A41, FUNCT_1:def 3;

        end;

         {} in O1 by A4, ORDINAL3: 8;

        then

        reconsider RTs = ( rng Ts) as non empty set by A34, FUNCT_1: 3;

        reconsider f as Function by A33;

        

         A42: ( dom f) = ( union ( rng ( doms LsF))) by Th1;

        

         A43: YY = { [:a, a:] where a be Element of RTs : a in RTs }

        proof

          set XX = { [:a, a:] where a be Element of RTs : a in RTs };

          thus YY c= XX

          proof

            let Z be object;

            assume Z in YY;

            then

            consider o be Element of o1 such that

             A44: Z = [:( ConsecutiveSet (A,o)), ( ConsecutiveSet (A,o)):];

            (Ts . o) = ( ConsecutiveSet (A,o)) by A34;

            then

            reconsider CoS = ( ConsecutiveSet (A,o)) as Element of RTs by A34, FUNCT_1:def 3;

            Z = [:CoS, CoS:] by A44;

            hence thesis;

          end;

          let Z be object;

          assume Z in XX;

          then

          consider a be Element of RTs such that

           A45: Z = [:a, a:] and a in RTs;

          consider o be object such that

           A46: o in ( dom Ts) and

           A47: a = (Ts . o) by FUNCT_1:def 3;

          reconsider o9 = o as Ordinal by A46;

          a = ( ConsecutiveSet (A,o9)) by A34, A46, A47;

          hence thesis by A34, A45, A46;

        end;

        for x,y be set st x in RTs & y in RTs holds (x,y) are_c=-comparable

        proof

          let x,y be set;

          assume that

           A48: x in RTs and

           A49: y in RTs;

          consider o1 be object such that

           A50: o1 in ( dom Ts) and

           A51: (Ts . o1) = x by A48, FUNCT_1:def 3;

          consider o2 be object such that

           A52: o2 in ( dom Ts) and

           A53: (Ts . o2) = y by A49, FUNCT_1:def 3;

          reconsider o19 = o1, o29 = o2 as Ordinal by A50, A52;

          

           A54: (Ts . o29) = ( ConsecutiveSet (A,o29)) by A34, A52;

          

           A55: o19 c= o29 or o29 c= o19;

          (Ts . o19) = ( ConsecutiveSet (A,o19)) by A34, A50;

          then x c= y or y c= x by A51, A53, A54, A55, Th29;

          hence thesis;

        end;

        then

         A56: RTs is c=-linear;

        

         A57: ( ConsecutiveDelta (q,O1)) = ( union ( rng Ls)) by A4, A5, A7, Th28;

        X = [:( union ( rng Ts)), ( ConsecutiveSet (A,O1)):] by A4, A5, A34, Th23

        .= [:( union RTs), ( union RTs):] by A4, A5, A34, Th23

        .= ( dom f) by A42, A36, A56, A43, Th3;

        hence thesis by A57, A33, FUNCT_2:def 1, RELSET_1: 4;

      end;

      ( ConsecutiveSet (A, {} )) = A by Th21;

      then

       A58: Y[ 0 ] by Th26;

      for O holds Y[O] from ORDINAL2:sch 1( A58, A1, A3);

      hence thesis;

    end;

    definition

      let A, L;

      let d be BiFunction of A, L;

      let q be QuadrSeq of d;

      let O;

      :: original: ConsecutiveDelta

      redefine

      func ConsecutiveDelta (q,O) -> BiFunction of ( ConsecutiveSet (A,O)), L ;

      coherence by Th30;

    end

    theorem :: LATTICE5:31

    

     Th31: for d be BiFunction of A, L holds for q be QuadrSeq of d holds d c= ( ConsecutiveDelta (q,O))

    proof

      let d be BiFunction of A, L;

      let q be QuadrSeq of d;

      defpred X[ Ordinal] means d c= ( ConsecutiveDelta (q,$1));

      

       A1: for O2 st O2 <> 0 & O2 is limit_ordinal & for O1 st O1 in O2 holds X[O1] holds X[O2]

      proof

        deffunc U( Ordinal) = ( ConsecutiveDelta (q,$1));

        let O2;

        assume that

         A2: O2 <> 0 and

         A3: O2 is limit_ordinal and for O1 st O1 in O2 holds d c= ( ConsecutiveDelta (q,O1));

        

         A4: {} in O2 by A2, ORDINAL3: 8;

        consider Ls be Sequence such that

         A5: ( dom Ls) = O2 & for O1 be Ordinal st O1 in O2 holds (Ls . O1) = U(O1) from ORDINAL2:sch 2;

        (Ls . {} ) = ( ConsecutiveDelta (q, {} )) by A2, A5, ORDINAL3: 8

        .= d by Th26;

        then

         A6: d in ( rng Ls) by A5, A4, FUNCT_1:def 3;

        ( ConsecutiveDelta (q,O2)) = ( union ( rng Ls)) by A2, A3, A5, Th28;

        hence thesis by A6, ZFMISC_1: 74;

      end;

      

       A7: for O1 st X[O1] holds X[( succ O1)]

      proof

        let O1;

        ( ConsecutiveDelta (q,( succ O1))) = ( new_bi_fun (( BiFun (( ConsecutiveDelta (q,O1)),( ConsecutiveSet (A,O1)),L)),( Quadr (q,O1)))) by Th27

        .= ( new_bi_fun (( ConsecutiveDelta (q,O1)),( Quadr (q,O1)))) by Def15;

        then

         A8: ( ConsecutiveDelta (q,O1)) c= ( ConsecutiveDelta (q,( succ O1))) by Th19;

        assume d c= ( ConsecutiveDelta (q,O1));

        hence thesis by A8, XBOOLE_1: 1;

      end;

      

       A9: X[ 0 ] by Th26;

      for O holds X[O] from ORDINAL2:sch 1( A9, A7, A1);

      hence thesis;

    end;

    theorem :: LATTICE5:32

    

     Th32: for d be BiFunction of A, L holds for q be QuadrSeq of d st O1 c= O2 holds ( ConsecutiveDelta (q,O1)) c= ( ConsecutiveDelta (q,O2))

    proof

      let d be BiFunction of A, L;

      let q be QuadrSeq of d;

      defpred X[ Ordinal] means O1 c= $1 implies ( ConsecutiveDelta (q,O1)) c= ( ConsecutiveDelta (q,$1));

      

       A1: for O2 st O2 <> 0 & O2 is limit_ordinal & for O3 st O3 in O2 holds X[O3] holds X[O2]

      proof

        deffunc U( Ordinal) = ( ConsecutiveDelta (q,$1));

        let O2;

        assume that

         A2: O2 <> 0 & O2 is limit_ordinal and for O3 st O3 in O2 holds O1 c= O3 implies ( ConsecutiveDelta (q,O1)) c= ( ConsecutiveDelta (q,O3));

        consider L be Sequence such that

         A3: ( dom L) = O2 & for O3 be Ordinal st O3 in O2 holds (L . O3) = U(O3) from ORDINAL2:sch 2;

        

         A4: ( ConsecutiveDelta (q,O2)) = ( union ( rng L)) by A2, A3, Th28;

        assume

         A5: O1 c= O2;

        per cases ;

          suppose O1 = O2;

          hence thesis;

        end;

          suppose O1 <> O2;

          then

           A6: O1 c< O2 by A5;

          then O1 in O2 by ORDINAL1: 11;

          then

           A7: (L . O1) in ( rng L) by A3, FUNCT_1:def 3;

          (L . O1) = ( ConsecutiveDelta (q,O1)) by A3, A6, ORDINAL1: 11;

          hence thesis by A4, A7, ZFMISC_1: 74;

        end;

      end;

      

       A8: for O2 st X[O2] holds X[( succ O2)]

      proof

        let O2;

        assume

         A9: O1 c= O2 implies ( ConsecutiveDelta (q,O1)) c= ( ConsecutiveDelta (q,O2));

        assume

         A10: O1 c= ( succ O2);

        per cases ;

          suppose O1 = ( succ O2);

          hence thesis;

        end;

          suppose O1 <> ( succ O2);

          then O1 c< ( succ O2) by A10;

          then

           A11: O1 in ( succ O2) by ORDINAL1: 11;

          ( ConsecutiveDelta (q,( succ O2))) = ( new_bi_fun (( BiFun (( ConsecutiveDelta (q,O2)),( ConsecutiveSet (A,O2)),L)),( Quadr (q,O2)))) by Th27

          .= ( new_bi_fun (( ConsecutiveDelta (q,O2)),( Quadr (q,O2)))) by Def15;

          then ( ConsecutiveDelta (q,O2)) c= ( ConsecutiveDelta (q,( succ O2))) by Th19;

          hence thesis by A9, A11, ORDINAL1: 22;

        end;

      end;

      

       A12: X[ 0 ];

      for O2 holds X[O2] from ORDINAL2:sch 1( A12, A8, A1);

      hence thesis;

    end;

    theorem :: LATTICE5:33

    

     Th33: for d be BiFunction of A, L st d is zeroed holds for q be QuadrSeq of d holds ( ConsecutiveDelta (q,O)) is zeroed

    proof

      let d be BiFunction of A, L;

      assume

       A1: d is zeroed;

      let q be QuadrSeq of d;

      defpred X[ Ordinal] means ( ConsecutiveDelta (q,$1)) is zeroed;

      

       A2: for O1 st X[O1] holds X[( succ O1)]

      proof

        let O1;

        assume ( ConsecutiveDelta (q,O1)) is zeroed;

        then

         A3: ( new_bi_fun (( ConsecutiveDelta (q,O1)),( Quadr (q,O1)))) is zeroed by Th16;

        let z be Element of ( ConsecutiveSet (A,( succ O1)));

        reconsider z9 = z as Element of ( new_set ( ConsecutiveSet (A,O1))) by Th22;

        ( ConsecutiveDelta (q,( succ O1))) = ( new_bi_fun (( BiFun (( ConsecutiveDelta (q,O1)),( ConsecutiveSet (A,O1)),L)),( Quadr (q,O1)))) by Th27

        .= ( new_bi_fun (( ConsecutiveDelta (q,O1)),( Quadr (q,O1)))) by Def15;

        

        hence (( ConsecutiveDelta (q,( succ O1))) . (z,z)) = (( new_bi_fun (( ConsecutiveDelta (q,O1)),( Quadr (q,O1)))) . (z9,z9))

        .= ( Bottom L) by A3;

      end;

      

       A4: for O2 st O2 <> 0 & O2 is limit_ordinal & for O1 st O1 in O2 holds X[O1] holds X[O2]

      proof

        deffunc U( Ordinal) = ( ConsecutiveDelta (q,$1));

        let O2;

        assume that

         A5: O2 <> 0 & O2 is limit_ordinal and

         A6: for O1 st O1 in O2 holds ( ConsecutiveDelta (q,O1)) is zeroed;

        set CS = ( ConsecutiveSet (A,O2));

        consider Ls be Sequence such that

         A7: ( dom Ls) = O2 & for O1 be Ordinal st O1 in O2 holds (Ls . O1) = U(O1) from ORDINAL2:sch 2;

        ( ConsecutiveDelta (q,O2)) = ( union ( rng Ls)) by A5, A7, Th28;

        then

        reconsider f = ( union ( rng Ls)) as BiFunction of CS, L;

        deffunc U( Ordinal) = ( ConsecutiveSet (A,$1));

        consider Ts be Sequence such that

         A8: ( dom Ts) = O2 & for O1 be Ordinal st O1 in O2 holds (Ts . O1) = U(O1) from ORDINAL2:sch 2;

        

         A9: ( ConsecutiveSet (A,O2)) = ( union ( rng Ts)) by A5, A8, Th23;

        f is zeroed

        proof

          let x be Element of CS;

          consider y be set such that

           A10: x in y and

           A11: y in ( rng Ts) by A9, TARSKI:def 4;

          consider o be object such that

           A12: o in ( dom Ts) and

           A13: y = (Ts . o) by A11, FUNCT_1:def 3;

          reconsider o as Ordinal by A12;

          

           A14: (Ls . o) = ( ConsecutiveDelta (q,o)) by A7, A8, A12;

          then

          reconsider h = (Ls . o) as BiFunction of ( ConsecutiveSet (A,o)), L;

          reconsider x9 = x as Element of ( ConsecutiveSet (A,o)) by A8, A10, A12, A13;

          

           A15: ( dom h) = [:( ConsecutiveSet (A,o)), ( ConsecutiveSet (A,o)):] by FUNCT_2:def 1;

          

           A16: h is zeroed

          proof

            let z be Element of ( ConsecutiveSet (A,o));

            

             A17: ( ConsecutiveDelta (q,o)) is zeroed by A6, A8, A12;

            

            thus (h . (z,z)) = (( ConsecutiveDelta (q,o)) . (z,z)) by A7, A8, A12

            .= ( Bottom L) by A17;

          end;

          ( ConsecutiveDelta (q,o)) in ( rng Ls) by A7, A8, A12, A14, FUNCT_1:def 3;

          then

           A18: h c= f by A14, ZFMISC_1: 74;

          x in ( ConsecutiveSet (A,o)) by A8, A10, A12, A13;

          then [x, x] in ( dom h) by A15, ZFMISC_1: 87;

          

          hence (f . (x,x)) = (h . (x9,x9)) by A18, GRFUNC_1: 2

          .= ( Bottom L) by A16;

        end;

        hence thesis by A5, A7, Th28;

      end;

      

       A19: X[ 0 ]

      proof

        let z be Element of ( ConsecutiveSet (A, 0 ));

        reconsider z9 = z as Element of A by Th21;

        

        thus (( ConsecutiveDelta (q, 0 )) . (z,z)) = (d . (z9,z9)) by Th26

        .= ( Bottom L) by A1;

      end;

      for O holds X[O] from ORDINAL2:sch 1( A19, A2, A4);

      hence thesis;

    end;

    theorem :: LATTICE5:34

    

     Th34: for d be BiFunction of A, L st d is symmetric holds for q be QuadrSeq of d holds ( ConsecutiveDelta (q,O)) is symmetric

    proof

      let d be BiFunction of A, L;

      assume

       A1: d is symmetric;

      let q be QuadrSeq of d;

      defpred X[ Ordinal] means ( ConsecutiveDelta (q,$1)) is symmetric;

      

       A2: for O1 st X[O1] holds X[( succ O1)]

      proof

        let O1;

        assume ( ConsecutiveDelta (q,O1)) is symmetric;

        then

         A3: ( new_bi_fun (( ConsecutiveDelta (q,O1)),( Quadr (q,O1)))) is symmetric by Th17;

        let x,y be Element of ( ConsecutiveSet (A,( succ O1)));

        reconsider x9 = x, y9 = y as Element of ( new_set ( ConsecutiveSet (A,O1))) by Th22;

        

         A4: ( ConsecutiveDelta (q,( succ O1))) = ( new_bi_fun (( BiFun (( ConsecutiveDelta (q,O1)),( ConsecutiveSet (A,O1)),L)),( Quadr (q,O1)))) by Th27

        .= ( new_bi_fun (( ConsecutiveDelta (q,O1)),( Quadr (q,O1)))) by Def15;

        

        hence (( ConsecutiveDelta (q,( succ O1))) . (x,y)) = (( new_bi_fun (( ConsecutiveDelta (q,O1)),( Quadr (q,O1)))) . (y9,x9)) by A3

        .= (( ConsecutiveDelta (q,( succ O1))) . (y,x)) by A4;

      end;

      

       A5: for O2 st O2 <> 0 & O2 is limit_ordinal & for O1 st O1 in O2 holds X[O1] holds X[O2]

      proof

        deffunc U( Ordinal) = ( ConsecutiveDelta (q,$1));

        let O2;

        assume that

         A6: O2 <> 0 & O2 is limit_ordinal and

         A7: for O1 st O1 in O2 holds ( ConsecutiveDelta (q,O1)) is symmetric;

        set CS = ( ConsecutiveSet (A,O2));

        consider Ls be Sequence such that

         A8: ( dom Ls) = O2 & for O1 be Ordinal st O1 in O2 holds (Ls . O1) = U(O1) from ORDINAL2:sch 2;

        ( ConsecutiveDelta (q,O2)) = ( union ( rng Ls)) by A6, A8, Th28;

        then

        reconsider f = ( union ( rng Ls)) as BiFunction of CS, L;

        deffunc U( Ordinal) = ( ConsecutiveSet (A,$1));

        consider Ts be Sequence such that

         A9: ( dom Ts) = O2 & for O1 be Ordinal st O1 in O2 holds (Ts . O1) = U(O1) from ORDINAL2:sch 2;

        

         A10: ( ConsecutiveSet (A,O2)) = ( union ( rng Ts)) by A6, A9, Th23;

        f is symmetric

        proof

          let x,y be Element of CS;

          consider x1 be set such that

           A11: x in x1 and

           A12: x1 in ( rng Ts) by A10, TARSKI:def 4;

          consider o1 be object such that

           A13: o1 in ( dom Ts) and

           A14: x1 = (Ts . o1) by A12, FUNCT_1:def 3;

          consider y1 be set such that

           A15: y in y1 and

           A16: y1 in ( rng Ts) by A10, TARSKI:def 4;

          consider o2 be object such that

           A17: o2 in ( dom Ts) and

           A18: y1 = (Ts . o2) by A16, FUNCT_1:def 3;

          reconsider o1, o2 as Ordinal by A13, A17;

          

           A19: x in ( ConsecutiveSet (A,o1)) by A9, A11, A13, A14;

          

           A20: (Ls . o1) = ( ConsecutiveDelta (q,o1)) by A8, A9, A13;

          then

          reconsider h1 = (Ls . o1) as BiFunction of ( ConsecutiveSet (A,o1)), L;

          

           A21: h1 is symmetric

          proof

            let x,y be Element of ( ConsecutiveSet (A,o1));

            

             A22: ( ConsecutiveDelta (q,o1)) is symmetric by A7, A9, A13;

            

            thus (h1 . (x,y)) = (( ConsecutiveDelta (q,o1)) . (x,y)) by A8, A9, A13

            .= (( ConsecutiveDelta (q,o1)) . (y,x)) by A22

            .= (h1 . (y,x)) by A8, A9, A13;

          end;

          

           A23: ( dom h1) = [:( ConsecutiveSet (A,o1)), ( ConsecutiveSet (A,o1)):] by FUNCT_2:def 1;

          

           A24: y in ( ConsecutiveSet (A,o2)) by A9, A15, A17, A18;

          

           A25: (Ls . o2) = ( ConsecutiveDelta (q,o2)) by A8, A9, A17;

          then

          reconsider h2 = (Ls . o2) as BiFunction of ( ConsecutiveSet (A,o2)), L;

          

           A26: h2 is symmetric

          proof

            let x,y be Element of ( ConsecutiveSet (A,o2));

            

             A27: ( ConsecutiveDelta (q,o2)) is symmetric by A7, A9, A17;

            

            thus (h2 . (x,y)) = (( ConsecutiveDelta (q,o2)) . (x,y)) by A8, A9, A17

            .= (( ConsecutiveDelta (q,o2)) . (y,x)) by A27

            .= (h2 . (y,x)) by A8, A9, A17;

          end;

          

           A28: ( dom h2) = [:( ConsecutiveSet (A,o2)), ( ConsecutiveSet (A,o2)):] by FUNCT_2:def 1;

          per cases ;

            suppose o1 c= o2;

            then

             A29: ( ConsecutiveSet (A,o1)) c= ( ConsecutiveSet (A,o2)) by Th29;

            then

             A30: [y, x] in ( dom h2) by A19, A24, A28, ZFMISC_1: 87;

            ( ConsecutiveDelta (q,o2)) in ( rng Ls) by A8, A9, A17, A25, FUNCT_1:def 3;

            then

             A31: h2 c= f by A25, ZFMISC_1: 74;

            reconsider x9 = x, y9 = y as Element of ( ConsecutiveSet (A,o2)) by A9, A15, A17, A18, A19, A29;

             [x, y] in ( dom h2) by A19, A24, A28, A29, ZFMISC_1: 87;

            

            hence (f . (x,y)) = (h2 . (x9,y9)) by A31, GRFUNC_1: 2

            .= (h2 . (y9,x9)) by A26

            .= (f . (y,x)) by A31, A30, GRFUNC_1: 2;

          end;

            suppose o2 c= o1;

            then

             A32: ( ConsecutiveSet (A,o2)) c= ( ConsecutiveSet (A,o1)) by Th29;

            then

             A33: [y, x] in ( dom h1) by A19, A24, A23, ZFMISC_1: 87;

            ( ConsecutiveDelta (q,o1)) in ( rng Ls) by A8, A9, A13, A20, FUNCT_1:def 3;

            then

             A34: h1 c= f by A20, ZFMISC_1: 74;

            reconsider x9 = x, y9 = y as Element of ( ConsecutiveSet (A,o1)) by A9, A11, A13, A14, A24, A32;

             [x, y] in ( dom h1) by A19, A24, A23, A32, ZFMISC_1: 87;

            

            hence (f . (x,y)) = (h1 . (x9,y9)) by A34, GRFUNC_1: 2

            .= (h1 . (y9,x9)) by A21

            .= (f . (y,x)) by A34, A33, GRFUNC_1: 2;

          end;

        end;

        hence thesis by A6, A8, Th28;

      end;

      

       A35: X[ 0 ]

      proof

        let x,y be Element of ( ConsecutiveSet (A, 0 ));

        reconsider x9 = x, y9 = y as Element of A by Th21;

        

        thus (( ConsecutiveDelta (q, 0 )) . (x,y)) = (d . (x9,y9)) by Th26

        .= (d . (y9,x9)) by A1

        .= (( ConsecutiveDelta (q, 0 )) . (y,x)) by Th26;

      end;

      for O holds X[O] from ORDINAL2:sch 1( A35, A2, A5);

      hence thesis;

    end;

    theorem :: LATTICE5:35

    

     Th35: for d be BiFunction of A, L st d is symmetric u.t.i. holds for q be QuadrSeq of d st O c= ( DistEsti d) holds ( ConsecutiveDelta (q,O)) is u.t.i.

    proof

      let d be BiFunction of A, L;

      assume that

       A1: d is symmetric and

       A2: d is u.t.i.;

      let q be QuadrSeq of d;

      defpred X[ Ordinal] means $1 c= ( DistEsti d) implies ( ConsecutiveDelta (q,$1)) is u.t.i.;

      

       A3: for O1 st X[O1] holds X[( succ O1)]

      proof

        let O1;

        assume that

         A4: O1 c= ( DistEsti d) implies ( ConsecutiveDelta (q,O1)) is u.t.i. and

         A5: ( succ O1) c= ( DistEsti d);

        

         A6: O1 in ( DistEsti d) by A5, ORDINAL1: 21;

        then

         A7: O1 in ( dom q) by Th25;

        then (q . O1) in ( rng q) by FUNCT_1:def 3;

        then

         A8: (q . O1) in { [u, v, a9, b9] where u be Element of A, v be Element of A, a9 be Element of L, b9 be Element of L : (d . (u,v)) <= (a9 "\/" b9) } by Def13;

        let x,y,z be Element of ( ConsecutiveSet (A,( succ O1)));

        

         A9: ( ConsecutiveDelta (q,O1)) is symmetric by A1, Th34;

        reconsider x9 = x, y9 = y, z9 = z as Element of ( new_set ( ConsecutiveSet (A,O1))) by Th22;

        set f = ( new_bi_fun (( ConsecutiveDelta (q,O1)),( Quadr (q,O1))));

        set X = (( Quadr (q,O1)) `1_4 ), Y = (( Quadr (q,O1)) `2_4 );

        reconsider a = (( Quadr (q,O1)) `3_4 ), b = (( Quadr (q,O1)) `4_4 ) as Element of L;

        

         A10: ( dom d) = [:A, A:] & d c= ( ConsecutiveDelta (q,O1)) by Th31, FUNCT_2:def 1;

        consider u,v be Element of A, a9,b9 be Element of L such that

         A11: (q . O1) = [u, v, a9, b9] and

         A12: (d . (u,v)) <= (a9 "\/" b9) by A8;

        

         A13: ( Quadr (q,O1)) = [u, v, a9, b9] by A7, A11, Def14;

        then

         A14: u = X & v = Y;

        

         A15: a9 = a & b9 = b by A13;

        (d . (u,v)) = (d . [u, v])

        .= (( ConsecutiveDelta (q,O1)) . (X,Y)) by A14, A10, GRFUNC_1: 2;

        then ( new_bi_fun (( ConsecutiveDelta (q,O1)),( Quadr (q,O1)))) is u.t.i. by A4, A6, A9, A12, A15, Th18, ORDINAL1:def 2;

        then

         A16: (f . (x9,z9)) <= ((f . (x9,y9)) "\/" (f . (y9,z9)));

        ( ConsecutiveDelta (q,( succ O1))) = ( new_bi_fun (( BiFun (( ConsecutiveDelta (q,O1)),( ConsecutiveSet (A,O1)),L)),( Quadr (q,O1)))) by Th27

        .= ( new_bi_fun (( ConsecutiveDelta (q,O1)),( Quadr (q,O1)))) by Def15;

        hence (( ConsecutiveDelta (q,( succ O1))) . (x,z)) <= ((( ConsecutiveDelta (q,( succ O1))) . (x,y)) "\/" (( ConsecutiveDelta (q,( succ O1))) . (y,z))) by A16;

      end;

      

       A17: for O2 st O2 <> 0 & O2 is limit_ordinal & for O1 st O1 in O2 holds X[O1] holds X[O2]

      proof

        deffunc U( Ordinal) = ( ConsecutiveDelta (q,$1));

        let O2;

        assume that

         A18: O2 <> 0 & O2 is limit_ordinal and

         A19: for O1 st O1 in O2 holds (O1 c= ( DistEsti d) implies ( ConsecutiveDelta (q,O1)) is u.t.i.) and

         A20: O2 c= ( DistEsti d);

        set CS = ( ConsecutiveSet (A,O2));

        consider Ls be Sequence such that

         A21: ( dom Ls) = O2 & for O1 be Ordinal st O1 in O2 holds (Ls . O1) = U(O1) from ORDINAL2:sch 2;

        ( ConsecutiveDelta (q,O2)) = ( union ( rng Ls)) by A18, A21, Th28;

        then

        reconsider f = ( union ( rng Ls)) as BiFunction of CS, L;

        deffunc U( Ordinal) = ( ConsecutiveSet (A,$1));

        consider Ts be Sequence such that

         A22: ( dom Ts) = O2 & for O1 be Ordinal st O1 in O2 holds (Ts . O1) = U(O1) from ORDINAL2:sch 2;

        

         A23: ( ConsecutiveSet (A,O2)) = ( union ( rng Ts)) by A18, A22, Th23;

        f is u.t.i.

        proof

          let x,y,z be Element of CS;

          consider X be set such that

           A24: x in X and

           A25: X in ( rng Ts) by A23, TARSKI:def 4;

          consider o1 be object such that

           A26: o1 in ( dom Ts) and

           A27: X = (Ts . o1) by A25, FUNCT_1:def 3;

          consider Y be set such that

           A28: y in Y and

           A29: Y in ( rng Ts) by A23, TARSKI:def 4;

          consider o2 be object such that

           A30: o2 in ( dom Ts) and

           A31: Y = (Ts . o2) by A29, FUNCT_1:def 3;

          consider Z be set such that

           A32: z in Z and

           A33: Z in ( rng Ts) by A23, TARSKI:def 4;

          consider o3 be object such that

           A34: o3 in ( dom Ts) and

           A35: Z = (Ts . o3) by A33, FUNCT_1:def 3;

          reconsider o1, o2, o3 as Ordinal by A26, A30, A34;

          

           A36: x in ( ConsecutiveSet (A,o1)) by A22, A24, A26, A27;

          

           A37: (Ls . o3) = ( ConsecutiveDelta (q,o3)) by A21, A22, A34;

          then

          reconsider h3 = (Ls . o3) as BiFunction of ( ConsecutiveSet (A,o3)), L;

          

           A38: h3 is u.t.i.

          proof

            let x,y,z be Element of ( ConsecutiveSet (A,o3));

            o3 c= ( DistEsti d) by A20, A22, A34, ORDINAL1:def 2;

            then

             A39: ( ConsecutiveDelta (q,o3)) is u.t.i. by A19, A22, A34;

            ( ConsecutiveDelta (q,o3)) = h3 by A21, A22, A34;

            hence (h3 . (x,z)) <= ((h3 . (x,y)) "\/" (h3 . (y,z))) by A39;

          end;

          

           A40: ( dom h3) = [:( ConsecutiveSet (A,o3)), ( ConsecutiveSet (A,o3)):] by FUNCT_2:def 1;

          

           A41: z in ( ConsecutiveSet (A,o3)) by A22, A32, A34, A35;

          

           A42: (Ls . o2) = ( ConsecutiveDelta (q,o2)) by A21, A22, A30;

          then

          reconsider h2 = (Ls . o2) as BiFunction of ( ConsecutiveSet (A,o2)), L;

          

           A43: h2 is u.t.i.

          proof

            let x,y,z be Element of ( ConsecutiveSet (A,o2));

            o2 c= ( DistEsti d) by A20, A22, A30, ORDINAL1:def 2;

            then

             A44: ( ConsecutiveDelta (q,o2)) is u.t.i. by A19, A22, A30;

            ( ConsecutiveDelta (q,o2)) = h2 by A21, A22, A30;

            hence (h2 . (x,z)) <= ((h2 . (x,y)) "\/" (h2 . (y,z))) by A44;

          end;

          

           A45: ( dom h2) = [:( ConsecutiveSet (A,o2)), ( ConsecutiveSet (A,o2)):] by FUNCT_2:def 1;

          

           A46: (Ls . o1) = ( ConsecutiveDelta (q,o1)) by A21, A22, A26;

          then

          reconsider h1 = (Ls . o1) as BiFunction of ( ConsecutiveSet (A,o1)), L;

          

           A47: h1 is u.t.i.

          proof

            let x,y,z be Element of ( ConsecutiveSet (A,o1));

            o1 c= ( DistEsti d) by A20, A22, A26, ORDINAL1:def 2;

            then

             A48: ( ConsecutiveDelta (q,o1)) is u.t.i. by A19, A22, A26;

            ( ConsecutiveDelta (q,o1)) = h1 by A21, A22, A26;

            hence (h1 . (x,z)) <= ((h1 . (x,y)) "\/" (h1 . (y,z))) by A48;

          end;

          

           A49: ( dom h1) = [:( ConsecutiveSet (A,o1)), ( ConsecutiveSet (A,o1)):] by FUNCT_2:def 1;

          

           A50: y in ( ConsecutiveSet (A,o2)) by A22, A28, A30, A31;

          per cases ;

            suppose

             A51: o1 c= o3;

            then

             A52: ( ConsecutiveSet (A,o1)) c= ( ConsecutiveSet (A,o3)) by Th29;

            thus ((f . (x,y)) "\/" (f . (y,z))) >= (f . (x,z))

            proof

              per cases ;

                suppose

                 A53: o2 c= o3;

                reconsider z9 = z as Element of ( ConsecutiveSet (A,o3)) by A22, A32, A34, A35;

                reconsider x9 = x as Element of ( ConsecutiveSet (A,o3)) by A36, A52;

                ( ConsecutiveDelta (q,o3)) in ( rng Ls) by A21, A22, A34, A37, FUNCT_1:def 3;

                then

                 A54: h3 c= f by A37, ZFMISC_1: 74;

                

                 A55: ( ConsecutiveSet (A,o2)) c= ( ConsecutiveSet (A,o3)) by A53, Th29;

                then

                reconsider y9 = y as Element of ( ConsecutiveSet (A,o3)) by A50;

                 [y, z] in ( dom h3) by A50, A41, A40, A55, ZFMISC_1: 87;

                then

                 A56: (f . (y,z)) = (h3 . (y9,z9)) by A54, GRFUNC_1: 2;

                 [x, z] in ( dom h3) by A36, A41, A40, A52, ZFMISC_1: 87;

                then

                 A57: (f . (x,z)) = (h3 . (x9,z9)) by A54, GRFUNC_1: 2;

                 [x, y] in ( dom h3) by A36, A50, A40, A52, A55, ZFMISC_1: 87;

                then (f . (x,y)) = (h3 . (x9,y9)) by A54, GRFUNC_1: 2;

                hence thesis by A38, A56, A57;

              end;

                suppose

                 A58: o3 c= o2;

                reconsider y9 = y as Element of ( ConsecutiveSet (A,o2)) by A22, A28, A30, A31;

                ( ConsecutiveDelta (q,o2)) in ( rng Ls) by A21, A22, A30, A42, FUNCT_1:def 3;

                then

                 A59: h2 c= f by A42, ZFMISC_1: 74;

                

                 A60: ( ConsecutiveSet (A,o3)) c= ( ConsecutiveSet (A,o2)) by A58, Th29;

                then

                reconsider z9 = z as Element of ( ConsecutiveSet (A,o2)) by A41;

                 [y, z] in ( dom h2) by A50, A41, A45, A60, ZFMISC_1: 87;

                then

                 A61: (f . (y,z)) = (h2 . (y9,z9)) by A59, GRFUNC_1: 2;

                ( ConsecutiveSet (A,o1)) c= ( ConsecutiveSet (A,o3)) by A51, Th29;

                then

                 A62: ( ConsecutiveSet (A,o1)) c= ( ConsecutiveSet (A,o2)) by A60;

                then

                reconsider x9 = x as Element of ( ConsecutiveSet (A,o2)) by A36;

                 [x, y] in ( dom h2) by A36, A50, A45, A62, ZFMISC_1: 87;

                then

                 A63: (f . (x,y)) = (h2 . (x9,y9)) by A59, GRFUNC_1: 2;

                 [x, z] in ( dom h2) by A36, A41, A45, A60, A62, ZFMISC_1: 87;

                then (f . (x,z)) = (h2 . (x9,z9)) by A59, GRFUNC_1: 2;

                hence thesis by A43, A63, A61;

              end;

            end;

          end;

            suppose

             A64: o3 c= o1;

            then

             A65: ( ConsecutiveSet (A,o3)) c= ( ConsecutiveSet (A,o1)) by Th29;

            thus ((f . (x,y)) "\/" (f . (y,z))) >= (f . (x,z))

            proof

              per cases ;

                suppose

                 A66: o1 c= o2;

                reconsider y9 = y as Element of ( ConsecutiveSet (A,o2)) by A22, A28, A30, A31;

                ( ConsecutiveDelta (q,o2)) in ( rng Ls) by A21, A22, A30, A42, FUNCT_1:def 3;

                then

                 A67: h2 c= f by A42, ZFMISC_1: 74;

                

                 A68: ( ConsecutiveSet (A,o1)) c= ( ConsecutiveSet (A,o2)) by A66, Th29;

                then

                reconsider x9 = x as Element of ( ConsecutiveSet (A,o2)) by A36;

                 [x, y] in ( dom h2) by A36, A50, A45, A68, ZFMISC_1: 87;

                then

                 A69: (f . (x,y)) = (h2 . (x9,y9)) by A67, GRFUNC_1: 2;

                ( ConsecutiveSet (A,o3)) c= ( ConsecutiveSet (A,o1)) by A64, Th29;

                then

                 A70: ( ConsecutiveSet (A,o3)) c= ( ConsecutiveSet (A,o2)) by A68;

                then

                reconsider z9 = z as Element of ( ConsecutiveSet (A,o2)) by A41;

                 [y, z] in ( dom h2) by A50, A41, A45, A70, ZFMISC_1: 87;

                then

                 A71: (f . (y,z)) = (h2 . (y9,z9)) by A67, GRFUNC_1: 2;

                 [x, z] in ( dom h2) by A36, A41, A45, A68, A70, ZFMISC_1: 87;

                then (f . (x,z)) = (h2 . (x9,z9)) by A67, GRFUNC_1: 2;

                hence thesis by A43, A69, A71;

              end;

                suppose

                 A72: o2 c= o1;

                reconsider x9 = x as Element of ( ConsecutiveSet (A,o1)) by A22, A24, A26, A27;

                reconsider z9 = z as Element of ( ConsecutiveSet (A,o1)) by A41, A65;

                ( ConsecutiveDelta (q,o1)) in ( rng Ls) by A21, A22, A26, A46, FUNCT_1:def 3;

                then

                 A73: h1 c= f by A46, ZFMISC_1: 74;

                

                 A74: ( ConsecutiveSet (A,o2)) c= ( ConsecutiveSet (A,o1)) by A72, Th29;

                then

                reconsider y9 = y as Element of ( ConsecutiveSet (A,o1)) by A50;

                 [x, y] in ( dom h1) by A36, A50, A49, A74, ZFMISC_1: 87;

                then

                 A75: (f . (x,y)) = (h1 . (x9,y9)) by A73, GRFUNC_1: 2;

                 [x, z] in ( dom h1) by A36, A41, A49, A65, ZFMISC_1: 87;

                then

                 A76: (f . (x,z)) = (h1 . (x9,z9)) by A73, GRFUNC_1: 2;

                 [y, z] in ( dom h1) by A50, A41, A49, A65, A74, ZFMISC_1: 87;

                then (f . (y,z)) = (h1 . (y9,z9)) by A73, GRFUNC_1: 2;

                hence thesis by A47, A75, A76;

              end;

            end;

          end;

        end;

        hence thesis by A18, A21, Th28;

      end;

      

       A77: X[ 0 ]

      proof

        assume 0 c= ( DistEsti d);

        let x,y,z be Element of ( ConsecutiveSet (A, 0 ));

        reconsider x9 = x, y9 = y, z9 = z as Element of A by Th21;

        ( ConsecutiveDelta (q, 0 )) = d & (d . (x9,z9)) <= ((d . (x9,y9)) "\/" (d . (y9,z9))) by A2, Th26;

        hence (( ConsecutiveDelta (q, 0 )) . (x,z)) <= ((( ConsecutiveDelta (q, 0 )) . (x,y)) "\/" (( ConsecutiveDelta (q, 0 )) . (y,z)));

      end;

      for O holds X[O] from ORDINAL2:sch 1( A77, A3, A17);

      hence thesis;

    end;

    theorem :: LATTICE5:36

    for d be distance_function of A, L holds for q be QuadrSeq of d st O c= ( DistEsti d) holds ( ConsecutiveDelta (q,O)) is distance_function of ( ConsecutiveSet (A,O)), L by Th33, Th34, Th35;

    definition

      let A, L;

      let d be BiFunction of A, L;

      :: LATTICE5:def17

      func NextSet (d) -> set equals ( ConsecutiveSet (A,( DistEsti d)));

      correctness ;

    end

    registration

      let A, L;

      let d be BiFunction of A, L;

      cluster ( NextSet d) -> non empty;

      coherence ;

    end

    definition

      let A, L;

      let d be BiFunction of A, L;

      let q be QuadrSeq of d;

      :: LATTICE5:def18

      func NextDelta (q) -> set equals ( ConsecutiveDelta (q,( DistEsti d)));

      correctness ;

    end

    definition

      let A, L;

      let d be distance_function of A, L;

      let q be QuadrSeq of d;

      :: original: NextDelta

      redefine

      func NextDelta (q) -> distance_function of ( NextSet d), L ;

      coherence by Th33, Th34, Th35;

    end

    definition

      let A, L;

      let d be distance_function of A, L;

      let Aq be non empty set, dq be distance_function of Aq, L;

      :: LATTICE5:def19

      pred Aq,dq is_extension_of A,d means ex q be QuadrSeq of d st Aq = ( NextSet d) & dq = ( NextDelta q);

    end

    theorem :: LATTICE5:37

    

     Th37: for d be distance_function of A, L holds for Aq be non empty set, dq be distance_function of Aq, L st (Aq,dq) is_extension_of (A,d) holds for x,y be Element of A, a,b be Element of L st (d . (x,y)) <= (a "\/" b) holds ex z1,z2,z3 be Element of Aq st (dq . (x,z1)) = a & (dq . (z2,z3)) = a & (dq . (z1,z2)) = b & (dq . (z3,y)) = b

    proof

      let d be distance_function of A, L;

      let Aq be non empty set, dq be distance_function of Aq, L;

      assume (Aq,dq) is_extension_of (A,d);

      then

      consider q be QuadrSeq of d such that

       A1: Aq = ( NextSet d) and

       A2: dq = ( NextDelta q);

      let x,y be Element of A;

      let a,b be Element of L;

      assume

       A3: (d . (x,y)) <= (a "\/" b);

      ( rng q) = { [x9, y9, a9, b9] where x9 be Element of A, y9 be Element of A, a9 be Element of L, b9 be Element of L : (d . (x9,y9)) <= (a9 "\/" b9) } by Def13;

      then [x, y, a, b] in ( rng q) by A3;

      then

      consider o be object such that

       A4: o in ( dom q) and

       A5: (q . o) = [x, y, a, b] by FUNCT_1:def 3;

      reconsider o as Ordinal by A4;

      

       A6: (q . o) = ( Quadr (q,o)) by A4, Def14;

      then

       A7: x = (( Quadr (q,o)) `1_4 ) by A5;

      

       A8: b = (( Quadr (q,o)) `4_4 ) by A5, A6;

      

       A9: y = (( Quadr (q,o)) `2_4 ) by A5, A6;

      

       A10: a = (( Quadr (q,o)) `3_4 ) by A5, A6;

      reconsider B = ( ConsecutiveSet (A,o)) as non empty set;

       {B} in { {B}, { {B}}, { { {B}}}} by ENUMSET1:def 1;

      then

       A11: {B} in (B \/ { {B}, { {B}}, { { {B}}}}) by XBOOLE_0:def 3;

      reconsider cd = ( ConsecutiveDelta (q,o)) as BiFunction of B, L;

      reconsider Q = ( Quadr (q,o)) as Element of [:B, B, the carrier of L, the carrier of L:];

      

       A12: { {B}} in { {B}, { {B}}, { { {B}}}} by ENUMSET1:def 1;

      then

       A13: { {B}} in ( new_set B) by XBOOLE_0:def 3;

      A c= B by Th24;

      then

      reconsider xo = x, yo = y as Element of B;

      

       A14: B c= ( new_set B) by XBOOLE_1: 7;

      reconsider x1 = xo, y1 = yo as Element of ( new_set B) by A14;

      

       A15: cd is zeroed by Th33;

      

       A16: { { {B}}} in { {B}, { {B}}, { { {B}}}} by ENUMSET1:def 1;

      then

       A17: { { {B}}} in ( new_set B) by XBOOLE_0:def 3;

      o in ( DistEsti d) by A4, Th25;

      then

       A18: ( succ o) c= ( DistEsti d) by ORDINAL1: 21;

      then

       A19: ( ConsecutiveDelta (q,( succ o))) c= ( ConsecutiveDelta (q,( DistEsti d))) by Th32;

      ( ConsecutiveSet (A,( succ o))) = ( new_set B) by Th22;

      then ( new_set B) c= ( ConsecutiveSet (A,( DistEsti d))) by A18, Th29;

      then

      reconsider z1 = {B}, z2 = { {B}}, z3 = { { {B}}} as Element of Aq by A1, A11, A13, A17;

      take z1, z2, z3;

      

       A20: ( ConsecutiveDelta (q,( succ o))) = ( new_bi_fun (( BiFun (( ConsecutiveDelta (q,o)),( ConsecutiveSet (A,o)),L)),( Quadr (q,o)))) by Th27

      .= ( new_bi_fun (cd,Q)) by Def15;

      

       A21: ( dom ( new_bi_fun (cd,Q))) = [:( new_set B), ( new_set B):] by FUNCT_2:def 1;

      then [x1, {B}] in ( dom ( new_bi_fun (cd,Q))) by A11, ZFMISC_1: 87;

      

      hence (dq . (x,z1)) = (( new_bi_fun (cd,Q)) . (x1, {B})) by A2, A19, A20, GRFUNC_1: 2

      .= ((cd . (xo,xo)) "\/" a) by A7, A10, Def10

      .= (( Bottom L) "\/" a) by A15

      .= a by WAYBEL_1: 3;

       { {B}} in (B \/ { {B}, { {B}}, { { {B}}}}) by A12, XBOOLE_0:def 3;

      then [ { {B}}, { { {B}}}] in ( dom ( new_bi_fun (cd,Q))) by A17, A21, ZFMISC_1: 87;

      

      hence (dq . (z2,z3)) = (( new_bi_fun (cd,Q)) . ( { {B}}, { { {B}}})) by A2, A19, A20, GRFUNC_1: 2

      .= a by A10, Def10;

       [ {B}, { {B}}] in ( dom ( new_bi_fun (cd,Q))) by A11, A13, A21, ZFMISC_1: 87;

      

      hence (dq . (z1,z2)) = (( new_bi_fun (cd,Q)) . ( {B}, { {B}})) by A2, A19, A20, GRFUNC_1: 2

      .= b by A8, Def10;

       { { {B}}} in (B \/ { {B}, { {B}}, { { {B}}}}) by A16, XBOOLE_0:def 3;

      then [ { { {B}}}, y1] in ( dom ( new_bi_fun (cd,Q))) by A21, ZFMISC_1: 87;

      

      hence (dq . (z3,y)) = (( new_bi_fun (cd,Q)) . ( { { {B}}},y1)) by A2, A19, A20, GRFUNC_1: 2

      .= ((cd . (yo,yo)) "\/" b) by A9, A8, Def10

      .= (( Bottom L) "\/" b) by A15

      .= b by WAYBEL_1: 3;

    end;

    definition

      let A, L;

      let d be distance_function of A, L;

      :: LATTICE5:def20

      mode ExtensionSeq of A,d -> Function means

      : Def20: ( dom it ) = NAT & (it . 0 ) = [A, d] & for n be Nat holds ex A9 be non empty set, d9 be distance_function of A9, L, Aq be non empty set, dq be distance_function of Aq, L st (Aq,dq) is_extension_of (A9,d9) & (it . n) = [A9, d9] & (it . (n + 1)) = [Aq, dq];

      existence

      proof

        defpred P[ set, set, set] means (ex A9 be non empty set, d9 be distance_function of A9, L, Aq be non empty set, dq be distance_function of Aq, L st (Aq,dq) is_extension_of (A9,d9) & $2 = [A9, d9] & $3 = [Aq, dq]) or $3 = 0 & not ex A9 be non empty set, d9 be distance_function of A9, L, Aq be non empty set, dq be distance_function of Aq, L st (Aq,dq) is_extension_of (A9,d9) & $2 = [A9, d9];

        

         A1: for n be Nat holds for x be set holds ex y be set st P[n, x, y]

        proof

          let n be Nat;

          let x be set;

          per cases ;

            suppose ex A9 be non empty set, d9 be distance_function of A9, L, Aq be non empty set, dq be distance_function of Aq, L st (Aq,dq) is_extension_of (A9,d9) & x = [A9, d9];

            then

            consider A9 be non empty set, d9 be distance_function of A9, L, Aq be non empty set, dq be distance_function of Aq, L such that

             A2: (Aq,dq) is_extension_of (A9,d9) & x = [A9, d9];

            take [Aq, dq];

            thus thesis by A2;

          end;

            suppose

             A3: not ex A9 be non empty set, d9 be distance_function of A9, L, Aq be non empty set, dq be distance_function of Aq, L st (Aq,dq) is_extension_of (A9,d9) & x = [A9, d9];

            take 0 ;

            thus thesis by A3;

          end;

        end;

        consider f be Function such that

         A4: ( dom f) = NAT and

         A5: (f . 0 ) = [A, d] and

         A6: for n be Nat holds P[n, (f . n), (f . (n + 1))] from RECDEF_1:sch 1( A1);

        take f;

        thus ( dom f) = NAT by A4;

        thus (f . 0 ) = [A, d] by A5;

        defpred X[ Nat] means ex A9 be non empty set, d9 be distance_function of A9, L, Aq be non empty set, dq be distance_function of Aq, L st (Aq,dq) is_extension_of (A9,d9) & (f . $1) = [A9, d9] & (f . ($1 + 1)) = [Aq, dq];

        

         A7: for k be Nat st X[k] holds X[(k + 1)]

        proof

          let k be Nat;

          given A9 be non empty set, d9 be distance_function of A9, L, Aq be non empty set, dq be distance_function of Aq, L such that (Aq,dq) is_extension_of (A9,d9) and (f . k) = [A9, d9] and

           A8: (f . (k + 1)) = [Aq, dq];

          ex A1 be non empty set, d1 be distance_function of A1, L, AQ be non empty set, DQ be distance_function of AQ, L st (AQ,DQ) is_extension_of (A1,d1) & (f . (k + 1)) = [A1, d1]

          proof

            set Q = the QuadrSeq of dq;

            set AQ = ( NextSet dq);

            take Aq, dq;

            set DQ = ( NextDelta Q);

            take AQ, DQ;

            thus (AQ,DQ) is_extension_of (Aq,dq);

            thus thesis by A8;

          end;

          hence thesis by A6;

        end;

        ex A9 be non empty set, d9 be distance_function of A9, L, Aq be non empty set, dq be distance_function of Aq, L st (Aq,dq) is_extension_of (A9,d9) & (f . 0 ) = [A9, d9]

        proof

          set Aq = ( NextSet d);

          set q = the QuadrSeq of d;

          take A, d;

          consider dq be distance_function of Aq, L such that

           A9: dq = ( NextDelta q);

          take Aq, dq;

          thus (Aq,dq) is_extension_of (A,d) by A9;

          thus thesis by A5;

        end;

        then

         A10: X[ 0 ] by A6;

        thus for k be Nat holds X[k] from NAT_1:sch 2( A10, A7);

      end;

    end

    theorem :: LATTICE5:38

    

     Th38: for d be distance_function of A, L holds for S be ExtensionSeq of A, d holds for k,l be Nat st k <= l holds ((S . k) `1 ) c= ((S . l) `1 )

    proof

      let d be distance_function of A, L;

      let S be ExtensionSeq of A, d;

      let k be Nat;

      defpred X[ Nat] means k <= $1 implies ((S . k) `1 ) c= ((S . $1) `1 );

      

       A1: for i be Nat st X[i] holds X[(i + 1)]

      proof

        let i be Nat;

        assume that

         A2: k <= i implies ((S . k) `1 ) c= ((S . i) `1 ) and

         A3: k <= (i + 1);

        per cases by A3, NAT_1: 8;

          suppose k = (i + 1);

          hence thesis;

        end;

          suppose

           A4: k <= i;

          consider A9 be non empty set, d9 be distance_function of A9, L, Aq be non empty set, dq be distance_function of Aq, L such that

           A5: (Aq,dq) is_extension_of (A9,d9) and

           A6: (S . i) = [A9, d9] and

           A7: (S . (i + 1)) = [Aq, dq] by Def20;

          

           A8: ((S . i) `1 ) c= ( ConsecutiveSet (A9,( DistEsti d9))) by Th24, A6;

          ex q be QuadrSeq of d9 st Aq = ( NextSet d9) & dq = ( NextDelta q) by A5;

          then ((S . (i + 1)) `1 ) = ( ConsecutiveSet (A9,( DistEsti d9))) by A7;

          hence thesis by A2, A4, A8;

        end;

      end;

      

       A9: X[ 0 ] by NAT_1: 3;

      thus for l be Nat holds X[l] from NAT_1:sch 2( A9, A1);

    end;

    theorem :: LATTICE5:39

    

     Th39: for d be distance_function of A, L holds for S be ExtensionSeq of A, d holds for k,l be Nat st k <= l holds ((S . k) `2 ) c= ((S . l) `2 )

    proof

      let d be distance_function of A, L;

      let S be ExtensionSeq of A, d;

      let k be Nat;

      defpred X[ Nat] means k <= $1 implies ((S . k) `2 ) c= ((S . $1) `2 );

      

       A1: for i be Nat st X[i] holds X[(i + 1)]

      proof

        let i be Nat;

        assume that

         A2: k <= i implies ((S . k) `2 ) c= ((S . i) `2 ) and

         A3: k <= (i + 1);

        per cases by A3, NAT_1: 8;

          suppose k = (i + 1);

          hence thesis;

        end;

          suppose

           A4: k <= i;

          consider A9 be non empty set, d9 be distance_function of A9, L, Aq be non empty set, dq be distance_function of Aq, L such that

           A5: (Aq,dq) is_extension_of (A9,d9) and

           A6: (S . i) = [A9, d9] and

           A7: (S . (i + 1)) = [Aq, dq] by Def20;

          consider q be QuadrSeq of d9 such that Aq = ( NextSet d9) and

           A8: dq = ( NextDelta q) by A5;

          

           A9: ((S . i) `2 ) c= ( ConsecutiveDelta (q,( DistEsti d9))) by Th31, A6;

          ((S . (i + 1)) `2 ) = ( ConsecutiveDelta (q,( DistEsti d9))) by A7, A8;

          hence thesis by A2, A4, A9;

        end;

      end;

      

       A10: X[ 0 ] by NAT_1: 3;

      thus for l be Nat holds X[l] from NAT_1:sch 2( A10, A1);

    end;

    definition

      let L;

      :: LATTICE5:def21

      func BasicDF (L) -> distance_function of the carrier of L, L means

      : Def21: for x,y be Element of L holds (x <> y implies (it . (x,y)) = (x "\/" y)) & (x = y implies (it . (x,y)) = ( Bottom L));

      existence

      proof

        defpred X[ Element of L, Element of L, set] means ($1 = $2 implies $3 = ( Bottom L)) & ($1 <> $2 implies $3 = ($1 "\/" $2));

        set A = the carrier of L;

        

         A1: for x,y be Element of L holds ex z be Element of L st X[x, y, z]

        proof

          let x,y be Element of L;

          per cases ;

            suppose

             A2: x = y;

            take ( Bottom L);

            thus thesis by A2;

          end;

            suppose

             A3: x <> y;

            take (x "\/" y);

            thus thesis by A3;

          end;

        end;

        consider f be Function of [:the carrier of L, the carrier of L:], the carrier of L such that

         A4: for x,y be Element of L holds X[x, y, (f . (x,y))] from BINOP_1:sch 3( A1);

        reconsider f as BiFunction of A, L;

        

         A5: f is zeroed by A4;

        

         A6: f is u.t.i.

        proof

          let x,y,z be Element of A;

          reconsider x9 = x, y9 = y, z9 = z as Element of L;

          per cases ;

            suppose

             A7: x = z;

            ((f . (x,y)) "\/" (f . (y,z))) >= ( Bottom L) by YELLOW_0: 44;

            hence thesis by A4, A7;

          end;

            suppose

             A8: x <> z;

            thus ((f . (x,y)) "\/" (f . (y,z))) >= (f . (x,z))

            proof

              per cases ;

                suppose

                 A9: x = y;

                (x9 "\/" z9) >= (x9 "\/" z9) by ORDERS_2: 1;

                then (f . (x,z)) >= (x9 "\/" z9) by A4, A8;

                then (( Bottom L) "\/" (f . (x,z))) >= (x9 "\/" z9) by WAYBEL_1: 3;

                then ((f . (x,y)) "\/" (f . (y,z))) >= (x9 "\/" z9) by A4, A9;

                hence thesis by A4, A8;

              end;

                suppose

                 A10: x <> y;

                ((x9 "\/" y9) "\/" (f . (y,z))) >= (x9 "\/" z9)

                proof

                  per cases ;

                    suppose

                     A11: y = z;

                    (x9 "\/" y9) >= (x9 "\/" y9) by ORDERS_2: 1;

                    then (( Bottom L) "\/" (x9 "\/" y9)) >= (x9 "\/" z9) by A11, WAYBEL_1: 3;

                    hence thesis by A4, A11;

                  end;

                    suppose

                     A12: y <> z;

                    ((x9 "\/" z9) "\/" y9) = ((x9 "\/" z9) "\/" (y9 "\/" y9)) by YELLOW_5: 1

                    .= (x9 "\/" (z9 "\/" (y9 "\/" y9))) by LATTICE3: 14

                    .= (x9 "\/" (y9 "\/" (y9 "\/" z9))) by LATTICE3: 14

                    .= ((x9 "\/" y9) "\/" (y9 "\/" z9)) by LATTICE3: 14;

                    then ((x9 "\/" y9) "\/" (y9 "\/" z9)) >= (x9 "\/" z9) by YELLOW_0: 22;

                    hence thesis by A4, A12;

                  end;

                end;

                then ((f . (x,y)) "\/" (f . (y,z))) >= (x9 "\/" z9) by A4, A10;

                hence thesis by A4, A8;

              end;

            end;

          end;

        end;

        f is symmetric

        proof

          let x,y be Element of A;

          reconsider x9 = x, y9 = y as Element of L;

          per cases ;

            suppose x = y;

            hence thesis;

          end;

            suppose

             A13: x <> y;

            

            hence (f . (x,y)) = (y9 "\/" x9) by A4

            .= (f . (y,x)) by A4, A13;

          end;

        end;

        then

        reconsider f as distance_function of A, L by A5, A6;

        take f;

        thus thesis by A4;

      end;

      uniqueness

      proof

        let f1,f2 be distance_function of the carrier of L, L such that

         A14: for x,y be Element of L holds (x <> y implies (f1 . (x,y)) = (x "\/" y)) & (x = y implies (f1 . (x,y)) = ( Bottom L)) and

         A15: for x,y be Element of L holds (x <> y implies (f2 . (x,y)) = (x "\/" y)) & (x = y implies (f2 . (x,y)) = ( Bottom L));

        

         A16: for z be object st z in ( dom f1) holds (f1 . z) = (f2 . z)

        proof

          let z be object;

          assume

           A17: z in ( dom f1);

          then

          consider x,y be object such that

           A18: z = [x, y] by RELAT_1:def 1;

          reconsider x, y as Element of L by A17, A18, ZFMISC_1: 87;

          per cases ;

            suppose

             A19: x = y;

            

            thus (f1 . z) = (f1 . (x,y)) by A18

            .= ( Bottom L) by A14, A19

            .= (f2 . (x,y)) by A15, A19

            .= (f2 . z) by A18;

          end;

            suppose

             A20: x <> y;

            

            thus (f1 . z) = (f1 . (x,y)) by A18

            .= (x "\/" y) by A14, A20

            .= (f2 . (x,y)) by A15, A20

            .= (f2 . z) by A18;

          end;

        end;

        ( dom f1) = [:the carrier of L, the carrier of L:] by FUNCT_2:def 1

        .= ( dom f2) by FUNCT_2:def 1;

        hence f1 = f2 by A16, FUNCT_1: 2;

      end;

    end

    theorem :: LATTICE5:40

    

     Th40: ( BasicDF L) is onto

    proof

      set X = the carrier of L, f = ( BasicDF L);

      for w be object st w in X holds ex z be object st z in [:X, X:] & w = (f . z)

      proof

        let w be object;

        assume

         A1: w in X;

        then

        reconsider w9 = w as Element of L;

        reconsider w99 = w as Element of L by A1;

        per cases ;

          suppose

           A2: w = ( Bottom L);

          reconsider z = [w, w] as set;

          take z;

          thus z in [:X, X:] by A1, ZFMISC_1: 87;

          

          thus (f . z) = (f . (w9,w9))

          .= w by A2, Def21;

        end;

          suppose

           A3: w <> ( Bottom L);

          reconsider z = [( Bottom L), w] as set;

          take z;

          thus z in [:X, X:] by A1, ZFMISC_1: 87;

          

          thus (f . z) = (f . (( Bottom L),w9))

          .= (( Bottom L) "\/" w99) by A3, Def21

          .= w by WAYBEL_1: 3;

        end;

      end;

      then ( rng f) = the carrier of L by FUNCT_2: 10;

      hence thesis by FUNCT_2:def 3;

    end;

     Lm2:

    now

      let j be Nat;

      assume that

       A1: 1 <= j and

       A2: j < 5;

      j < (4 + 1) by A2;

      then j <= 4 by NAT_1: 13;

      then j = 0 or ... or j = 4 by NAT_1: 60;

      hence j = 1 or ... or j = 4 by A1;

    end;

     Lm3:

    now

      let m be Element of NAT ;

      assume

       A1: m in ( Seg 5);

      then m <= 5 by FINSEQ_1: 1;

      then m = 0 or ... or m = 5 by NAT_1: 60;

      hence m = 1 or ... or m = 5 by A1, FINSEQ_1: 1;

    end;

     Lm4:

    now

      let A, L;

      let d be distance_function of A, L;

      ( succ {} ) c= ( DistEsti d) or ( DistEsti d) in ( succ {} ) by ORDINAL1: 16;

      then ( succ {} ) c= ( DistEsti d) or ( DistEsti d) c= {} by ORDINAL1: 22;

      hence ( succ {} ) c= ( DistEsti d) by Th20, XBOOLE_1: 3;

    end;

    theorem :: LATTICE5:41

    

     Th41: for S be ExtensionSeq of the carrier of L, ( BasicDF L) holds for FS be non empty set st FS = ( union the set of all ((S . i) `1 ) where i be Element of NAT ) holds ( union the set of all ((S . i) `2 ) where i be Element of NAT ) is distance_function of FS, L

    proof

      let S be ExtensionSeq of the carrier of L, ( BasicDF L);

      let FS be non empty set;

      assume

       A1: FS = ( union the set of all ((S . i) `1 ) where i be Element of NAT );

      reconsider FS as non empty set;

      set A = the carrier of L;

      set FD = ( union the set of all ((S . i) `2 ) where i be Element of NAT );

      now

        let x,y be set;

        assume that

         A2: x in the set of all ((S . i) `2 ) where i be Element of NAT and

         A3: y in the set of all ((S . i) `2 ) where i be Element of NAT ;

        consider k be Element of NAT such that

         A4: x = ((S . k) `2 ) by A2;

        consider l be Element of NAT such that

         A5: y = ((S . l) `2 ) by A3;

        k <= l or l <= k;

        then x c= y or y c= x by A4, A5, Th39;

        hence (x,y) are_c=-comparable ;

      end;

      then

       A6: the set of all ((S . i) `2 ) where i be Element of NAT is c=-linear;

       the set of all ((S . i) `2 ) where i be Element of NAT c= ( PFuncs ( [:FS, FS:],A))

      proof

        let z be object;

        assume z in the set of all ((S . i) `2 ) where i be Element of NAT ;

        then

        consider j be Element of NAT such that

         A7: z = ((S . j) `2 );

        consider A9 be non empty set, d9 be distance_function of A9, L, Aq be non empty set, dq be distance_function of Aq, L such that (Aq,dq) is_extension_of (A9,d9) and

         A8: (S . j) = [A9, d9] and (S . (j + 1)) = [Aq, dq] by Def20;

        A9 = ( [A9, d9] `1 );

        then A9 in the set of all ((S . i) `1 ) where i be Element of NAT by A8;

        then ( dom d9) = [:A9, A9:] & A9 c= FS by A1, FUNCT_2:def 1, ZFMISC_1: 74;

        then

         A9: ( rng d9) c= A & ( dom d9) c= [:FS, FS:] by ZFMISC_1: 96;

        z = d9 by A7, A8;

        hence thesis by A9, PARTFUN1:def 3;

      end;

      then FD in ( PFuncs ( [:FS, FS:],A)) by A6, TREES_2: 40;

      then

       A10: ex g be Function st FD = g & ( dom g) c= [:FS, FS:] & ( rng g) c= A by PARTFUN1:def 3;

      ((S . 0 ) `1 ) in the set of all ((S . i) `1 ) where i be Element of NAT ;

      then

      reconsider X = the set of all ((S . i) `1 ) where i be Element of NAT as non empty set;

      set LL = { [:I, I:] where I be Element of X : I in X }, PP = the set of all [:((S . i) `1 ), ((S . i) `1 ):] where i be Element of NAT ;

      defpred X[ object, object] means $2 = ((S . $1) `2 );

      

       A11: LL = PP

      proof

        thus LL c= PP

        proof

          let x be object;

          assume x in LL;

          then

          consider J be Element of X such that

           A12: x = [:J, J:] and

           A13: J in X;

          ex j be Element of NAT st J = ((S . j) `1 ) by A13;

          hence thesis by A12;

        end;

        let x be object;

        assume x in PP;

        then

        consider j be Element of NAT such that

         A14: x = [:((S . j) `1 ), ((S . j) `1 ):];

        ((S . j) `1 ) in X;

        hence thesis by A14;

      end;

      reconsider FD as Function by A10;

      

       A15: for x be object st x in NAT holds ex y be object st X[x, y];

      consider F be Function such that

       A16: ( dom F) = NAT and

       A17: for x be object st x in NAT holds X[x, (F . x)] from CLASSES1:sch 1( A15);

      

       A18: ( rng F) = the set of all ((S . i) `2 ) where i be Element of NAT

      proof

        thus ( rng F) c= the set of all ((S . i) `2 ) where i be Element of NAT

        proof

          let x be object;

          assume x in ( rng F);

          then

          consider j be object such that

           A19: j in ( dom F) and

           A20: (F . j) = x by FUNCT_1:def 3;

          reconsider j as Element of NAT by A16, A19;

          x = ((S . j) `2 ) by A17, A20;

          hence thesis;

        end;

        let x be object;

        assume x in the set of all ((S . i) `2 ) where i be Element of NAT ;

        then

        consider j be Element of NAT such that

         A21: x = ((S . j) `2 );

        x = (F . j) by A17, A21;

        hence thesis by A16, FUNCT_1:def 3;

      end;

      F is Function-yielding

      proof

        let x be object;

        assume x in ( dom F);

        then

        reconsider j = x as Element of NAT by A16;

        consider A1 be non empty set, d1 be distance_function of A1, L, Aq1 be non empty set, dq1 be distance_function of Aq1, L such that (Aq1,dq1) is_extension_of (A1,d1) and

         A22: (S . j) = [A1, d1] and (S . (j + 1)) = [Aq1, dq1] by Def20;

        ( [A1, d1] `2 ) = d1;

        hence thesis by A17, A22;

      end;

      then

      reconsider F as Function-yielding Function;

      

       A23: ( rng ( doms F)) = PP

      proof

        thus ( rng ( doms F)) c= PP

        proof

          let x be object;

          assume x in ( rng ( doms F));

          then

          consider j be object such that

           A24: j in ( dom ( doms F)) and

           A25: x = (( doms F) . j) by FUNCT_1:def 3;

          

           A26: j in ( dom F) by A24, FUNCT_6: 59;

          reconsider j as Element of NAT by A16, A24, FUNCT_6: 59;

          consider A1 be non empty set, d1 be distance_function of A1, L, Aq1 be non empty set, dq1 be distance_function of Aq1, L such that (Aq1,dq1) is_extension_of (A1,d1) and

           A27: (S . j) = [A1, d1] and (S . (j + 1)) = [Aq1, dq1] by Def20;

          

           A28: ( [A1, d1] `2 ) = d1;

          x = ( dom (F . j)) by A25, A26, FUNCT_6: 22

          .= ( dom d1) by A17, A28, A27

          .= [:((S . j) `1 ), ((S . j) `1 ):] by A27, FUNCT_2:def 1;

          hence thesis;

        end;

        let x be object;

        assume x in PP;

        then

        consider j be Element of NAT such that

         A29: x = [:((S . j) `1 ), ((S . j) `1 ):];

        consider A1 be non empty set, d1 be distance_function of A1, L, Aq1 be non empty set, dq1 be distance_function of Aq1, L such that (Aq1,dq1) is_extension_of (A1,d1) and

         A30: (S . j) = [A1, d1] and (S . (j + 1)) = [Aq1, dq1] by Def20;

        

         A31: ( [A1, d1] `2 ) = d1;

        j in NAT ;

        then

         A32: j in ( dom ( doms F)) by A16, FUNCT_6: 59;

        x = ( dom d1) by A29, A30, FUNCT_2:def 1

        .= ( dom (F . j)) by A17, A31, A30

        .= (( doms F) . j) by A16, FUNCT_6: 22;

        hence thesis by A32, FUNCT_1:def 3;

      end;

      now

        let x,y be set;

        assume that

         A33: x in X and

         A34: y in X;

        consider k be Element of NAT such that

         A35: x = ((S . k) `1 ) by A33;

        consider l be Element of NAT such that

         A36: y = ((S . l) `1 ) by A34;

        k <= l or l <= k;

        then x c= y or y c= x by A35, A36, Th38;

        hence (x,y) are_c=-comparable ;

      end;

      then X is c=-linear;

      

      then [:FS, FS:] = ( union ( rng ( doms F))) by A1, A23, A11, Th3

      .= ( dom FD) by A18, Th1;

      then

      reconsider FD as BiFunction of FS, L by A10, FUNCT_2:def 1, RELSET_1: 4;

      

       A37: FD is symmetric

      proof

        let x,y be Element of FS;

        consider x1 be set such that

         A38: x in x1 and

         A39: x1 in X by A1, TARSKI:def 4;

        consider k be Element of NAT such that

         A40: x1 = ((S . k) `1 ) by A39;

        consider A1 be non empty set, d1 be distance_function of A1, L, Aq1 be non empty set, dq1 be distance_function of Aq1, L such that (Aq1,dq1) is_extension_of (A1,d1) and

         A41: (S . k) = [A1, d1] and (S . (k + 1)) = [Aq1, dq1] by Def20;

        

         A42: ( [A1, d1] `1 ) = A1;

        

         A43: x in A1 by A38, A40, A41;

        ( [A1, d1] `2 ) = d1;

        then d1 in the set of all ((S . i) `2 ) where i be Element of NAT by A41;

        then

         A44: d1 c= FD by ZFMISC_1: 74;

        consider y1 be set such that

         A45: y in y1 and

         A46: y1 in X by A1, TARSKI:def 4;

        consider l be Element of NAT such that

         A47: y1 = ((S . l) `1 ) by A46;

        consider A2 be non empty set, d2 be distance_function of A2, L, Aq2 be non empty set, dq2 be distance_function of Aq2, L such that (Aq2,dq2) is_extension_of (A2,d2) and

         A48: (S . l) = [A2, d2] and (S . (l + 1)) = [Aq2, dq2] by Def20;

        

         A49: ( [A2, d2] `1 ) = A2;

        

         A50: y in A2 by A45, A47, A48;

        ( [A2, d2] `2 ) = d2;

        then d2 in the set of all ((S . i) `2 ) where i be Element of NAT by A48;

        then

         A51: d2 c= FD by ZFMISC_1: 74;

        per cases ;

          suppose k <= l;

          then A1 c= A2 by A42, A49, Th38, A41, A48;

          then

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

          

           A52: ( dom d2) = [:A2, A2:] by FUNCT_2:def 1;

          

          hence (FD . (x,y)) = (d2 . [x9, y9]) by A51, GRFUNC_1: 2

          .= (d2 . (x9,y9))

          .= (d2 . (y9,x9)) by Def5

          .= (FD . [y9, x9]) by A51, A52, GRFUNC_1: 2

          .= (FD . (y,x));

        end;

          suppose l <= k;

          then A2 c= A1 by A42, A49, Th38, A48, A41;

          then

          reconsider x9 = x, y9 = y as Element of A1 by A38, A40, A41, A50;

          

           A53: ( dom d1) = [:A1, A1:] by FUNCT_2:def 1;

          

          hence (FD . (x,y)) = (d1 . [x9, y9]) by A44, GRFUNC_1: 2

          .= (d1 . (x9,y9))

          .= (d1 . (y9,x9)) by Def5

          .= (FD . [y9, x9]) by A44, A53, GRFUNC_1: 2

          .= (FD . (y,x));

        end;

      end;

      

       A54: FD is u.t.i.

      proof

        let x,y,z be Element of FS;

        consider x1 be set such that

         A55: x in x1 and

         A56: x1 in X by A1, TARSKI:def 4;

        consider k be Element of NAT such that

         A57: x1 = ((S . k) `1 ) by A56;

        consider A1 be non empty set, d1 be distance_function of A1, L, Aq1 be non empty set, dq1 be distance_function of Aq1, L such that (Aq1,dq1) is_extension_of (A1,d1) and

         A58: (S . k) = [A1, d1] and (S . (k + 1)) = [Aq1, dq1] by Def20;

        

         A59: x in A1 by A55, A57, A58;

        ( [A1, d1] `2 ) = d1;

        then d1 in the set of all ((S . i) `2 ) where i be Element of NAT by A58;

        then

         A60: d1 c= FD by ZFMISC_1: 74;

        

         A61: ( dom d1) = [:A1, A1:] by FUNCT_2:def 1;

        

         A62: ((S . k) `1 ) = A1 by A58;

        consider y1 be set such that

         A63: y in y1 and

         A64: y1 in X by A1, TARSKI:def 4;

        consider l be Element of NAT such that

         A65: y1 = ((S . l) `1 ) by A64;

        consider A2 be non empty set, d2 be distance_function of A2, L, Aq2 be non empty set, dq2 be distance_function of Aq2, L such that (Aq2,dq2) is_extension_of (A2,d2) and

         A66: (S . l) = [A2, d2] and (S . (l + 1)) = [Aq2, dq2] by Def20;

        

         A67: y in A2 by A63, A65, A66;

        ( [A2, d2] `2 ) = d2;

        then d2 in the set of all ((S . i) `2 ) where i be Element of NAT by A66;

        then

         A68: d2 c= FD by ZFMISC_1: 74;

        

         A69: ( dom d2) = [:A2, A2:] by FUNCT_2:def 1;

        

         A70: ( [A2, d2] `1 ) = A2;

        consider z1 be set such that

         A71: z in z1 and

         A72: z1 in X by A1, TARSKI:def 4;

        consider n be Element of NAT such that

         A73: z1 = ((S . n) `1 ) by A72;

        consider A3 be non empty set, d3 be distance_function of A3, L, Aq3 be non empty set, dq3 be distance_function of Aq3, L such that (Aq3,dq3) is_extension_of (A3,d3) and

         A74: (S . n) = [A3, d3] and (S . (n + 1)) = [Aq3, dq3] by Def20;

        

         A75: ( [A3, d3] `1 ) = A3;

        

         A76: z in A3 by A71, A73, A74;

        ( [A3, d3] `2 ) = d3;

        then d3 in the set of all ((S . i) `2 ) where i be Element of NAT by A74;

        then

         A77: d3 c= FD by ZFMISC_1: 74;

        

         A78: ( dom d3) = [:A3, A3:] by FUNCT_2:def 1;

        per cases ;

          suppose k <= l;

          then

           A79: A1 c= A2 by A62, A70, Th38, A66;

          thus ((FD . (x,y)) "\/" (FD . (y,z))) >= (FD . (x,z))

          proof

            per cases ;

              suppose l <= n;

              then

               A80: A2 c= A3 by A70, A75, Th38, A74, A66;

              then A1 c= A3 by A79;

              then

              reconsider x9 = x, y9 = y as Element of A3 by A59, A67, A80;

              reconsider z9 = z as Element of A3 by A76;

              

               A81: (FD . (y,z)) = (d3 . [y9, z9]) by A77, A78, GRFUNC_1: 2

              .= (d3 . (y9,z9));

              

               A82: (FD . (x,z)) = (d3 . [x9, z9]) by A77, A78, GRFUNC_1: 2

              .= (d3 . (x9,z9));

              (FD . (x,y)) = (d3 . [x9, y9]) by A77, A78, GRFUNC_1: 2

              .= (d3 . (x9,y9));

              hence thesis by A81, A82, Def7;

            end;

              suppose n <= l;

              then

               A83: A3 c= A2 by A70, A75, Th38, A74, A66;

              reconsider y9 = y as Element of A2 by A67;

              reconsider x9 = x as Element of A2 by A59, A79;

              reconsider z9 = z as Element of A2 by A76, A83;

              

               A84: (FD . (y,z)) = (d2 . [y9, z9]) by A68, A69, GRFUNC_1: 2

              .= (d2 . (y9,z9));

              

               A85: (FD . (x,z)) = (d2 . [x9, z9]) by A68, A69, GRFUNC_1: 2

              .= (d2 . (x9,z9));

              (FD . (x,y)) = (d2 . [x9, y9]) by A68, A69, GRFUNC_1: 2

              .= (d2 . (x9,y9));

              hence thesis by A84, A85, Def7;

            end;

          end;

        end;

          suppose l <= k;

          then

           A86: A2 c= A1 by A62, A70, Th38, A66;

          thus ((FD . (x,y)) "\/" (FD . (y,z))) >= (FD . (x,z))

          proof

            per cases ;

              suppose k <= n;

              then

               A87: A1 c= A3 by A62, A75, Th38, A74;

              then

               A88: A2 c= A3 by A86;

              reconsider x9 = x as Element of A3 by A59, A87;

              reconsider z9 = z as Element of A3 by A71, A73, A74;

              reconsider y9 = y as Element of A3 by A67, A88;

              

               A89: (FD . (y,z)) = (d3 . [y9, z9]) by A77, A78, GRFUNC_1: 2

              .= (d3 . (y9,z9));

              

               A90: (FD . (x,z)) = (d3 . [x9, z9]) by A77, A78, GRFUNC_1: 2

              .= (d3 . (x9,z9));

              (FD . (x,y)) = (d3 . [x9, y9]) by A77, A78, GRFUNC_1: 2

              .= (d3 . (x9,y9));

              hence thesis by A89, A90, Def7;

            end;

              suppose n <= k;

              then A3 c= A1 by A62, A75, Th38, A74;

              then

              reconsider x9 = x, y9 = y, z9 = z as Element of A1 by A55, A57, A58, A67, A76, A86;

              

               A91: (FD . (y,z)) = (d1 . [y9, z9]) by A60, A61, GRFUNC_1: 2

              .= (d1 . (y9,z9));

              

               A92: (FD . (x,z)) = (d1 . [x9, z9]) by A60, A61, GRFUNC_1: 2

              .= (d1 . (x9,z9));

              (FD . (x,y)) = (d1 . [x9, y9]) by A60, A61, GRFUNC_1: 2

              .= (d1 . (x9,y9));

              hence thesis by A91, A92, Def7;

            end;

          end;

        end;

      end;

      FD is zeroed

      proof

        let x be Element of FS;

        consider y be set such that

         A93: x in y and

         A94: y in X by A1, TARSKI:def 4;

        consider j be Element of NAT such that

         A95: y = ((S . j) `1 ) by A94;

        consider A1 be non empty set, d1 be distance_function of A1, L, Aq1 be non empty set, dq1 be distance_function of Aq1, L such that (Aq1,dq1) is_extension_of (A1,d1) and

         A96: (S . j) = [A1, d1] and (S . (j + 1)) = [Aq1, dq1] by Def20;

        reconsider x9 = x as Element of A1 by A93, A95, A96;

        ( [A1, d1] `2 ) = d1;

        then d1 in the set of all ((S . i) `2 ) where i be Element of NAT by A96;

        then

         A97: d1 c= FD by ZFMISC_1: 74;

        ( dom d1) = [:A1, A1:] by FUNCT_2:def 1;

        

        hence (FD . (x,x)) = (d1 . [x9, x9]) by A97, GRFUNC_1: 2

        .= (d1 . (x9,x9))

        .= ( Bottom L) by Def6;

      end;

      hence thesis by A37, A54;

    end;

    theorem :: LATTICE5:42

    

     Th42: for S be ExtensionSeq of the carrier of L, ( BasicDF L) holds for FS be non empty set, FD be distance_function of FS, L holds for x,y be Element of FS holds for a,b be Element of L st FS = ( union the set of all ((S . i) `1 ) where i be Element of NAT ) & FD = ( union the set of all ((S . i) `2 ) where i be Element of NAT ) & (FD . (x,y)) <= (a "\/" b) holds ex z1,z2,z3 be Element of FS st (FD . (x,z1)) = a & (FD . (z2,z3)) = a & (FD . (z1,z2)) = b & (FD . (z3,y)) = b

    proof

      let S be ExtensionSeq of the carrier of L, ( BasicDF L);

      let FS be non empty set, FD be distance_function of FS, L;

      let x,y be Element of FS;

      let a,b be Element of L;

      assume that

       A1: FS = ( union the set of all ((S . i) `1 ) where i be Element of NAT ) and

       A2: FD = ( union the set of all ((S . i) `2 ) where i be Element of NAT ) and

       A3: (FD . (x,y)) <= (a "\/" b);

      ((S . 0 ) `1 ) in the set of all ((S . i) `1 ) where i be Element of NAT ;

      then

      reconsider X = the set of all ((S . i) `1 ) where i be Element of NAT as non empty set;

      consider x1 be set such that

       A4: x in x1 and

       A5: x1 in X by A1, TARSKI:def 4;

      consider k be Element of NAT such that

       A6: x1 = ((S . k) `1 ) by A5;

      consider A1 be non empty set, d1 be distance_function of A1, L, Aq1 be non empty set, dq1 be distance_function of Aq1, L such that

       A7: (Aq1,dq1) is_extension_of (A1,d1) and

       A8: (S . k) = [A1, d1] and

       A9: (S . (k + 1)) = [Aq1, dq1] by Def20;

      

       A10: ( [A1, d1] `1 ) = A1;

      

       A11: x in A1 by A4, A6, A8;

      ( [A1, d1] `2 ) = d1;

      then d1 in the set of all ((S . i) `2 ) where i be Element of NAT by A8;

      then

       A12: d1 c= FD by A2, ZFMISC_1: 74;

      

       A13: ( [Aq1, dq1] `1 ) = Aq1;

      then Aq1 in the set of all ((S . i) `1 ) where i be Element of NAT by A9;

      then

       A14: Aq1 c= FS by A1, ZFMISC_1: 74;

      ( [Aq1, dq1] `2 ) = dq1;

      then dq1 in the set of all ((S . i) `2 ) where i be Element of NAT by A9;

      then

       A15: dq1 c= FD by A2, ZFMISC_1: 74;

      consider y1 be set such that

       A16: y in y1 and

       A17: y1 in X by A1, TARSKI:def 4;

      consider l be Element of NAT such that

       A18: y1 = ((S . l) `1 ) by A17;

      consider A2 be non empty set, d2 be distance_function of A2, L, Aq2 be non empty set, dq2 be distance_function of Aq2, L such that

       A19: (Aq2,dq2) is_extension_of (A2,d2) and

       A20: (S . l) = [A2, d2] and

       A21: (S . (l + 1)) = [Aq2, dq2] by Def20;

      

       A22: ( [A2, d2] `1 ) = A2;

      

       A23: y in A2 by A16, A18, A20;

      ( [A2, d2] `2 ) = d2;

      then d2 in the set of all ((S . i) `2 ) where i be Element of NAT by A20;

      then

       A24: d2 c= FD by A2, ZFMISC_1: 74;

      

       A25: ( [Aq2, dq2] `1 ) = Aq2;

      then Aq2 in the set of all ((S . i) `1 ) where i be Element of NAT by A21;

      then

       A26: Aq2 c= FS by A1, ZFMISC_1: 74;

      ( [Aq2, dq2] `2 ) = dq2;

      then dq2 in the set of all ((S . i) `2 ) where i be Element of NAT by A21;

      then

       A27: dq2 c= FD by A2, ZFMISC_1: 74;

      per cases ;

        suppose k <= l;

        then A1 c= A2 by A10, A22, Th38, A20, A8;

        then

        reconsider x9 = x, y9 = y as Element of A2 by A11, A16, A18, A20;

        A2 c= Aq2 by A22, A25, Th38, A20, A21, NAT_1: 11;

        then

        reconsider x99 = x9, y99 = y9 as Element of Aq2;

        ( dom d2) = [:A2, A2:] by FUNCT_2:def 1;

        

        then (FD . (x,y)) = (d2 . [x9, y9]) by A24, GRFUNC_1: 2

        .= (d2 . (x9,y9));

        then

        consider z1,z2,z3 be Element of Aq2 such that

         A28: (dq2 . (x,z1)) = a and

         A29: (dq2 . (z2,z3)) = a and

         A30: (dq2 . (z1,z2)) = b and

         A31: (dq2 . (z3,y)) = b by A3, A19, Th37;

        reconsider z19 = z1, z29 = z2, z39 = z3 as Element of FS by A26;

        take z19, z29, z39;

        

         A32: ( dom dq2) = [:Aq2, Aq2:] by FUNCT_2:def 1;

        

        hence (FD . (x,z19)) = (dq2 . [x99, z1]) by A27, GRFUNC_1: 2

        .= a by A28;

        

        thus (FD . (z29,z39)) = (dq2 . [z2, z3]) by A27, A32, GRFUNC_1: 2

        .= a by A29;

        

        thus (FD . (z19,z29)) = (dq2 . [z1, z2]) by A27, A32, GRFUNC_1: 2

        .= b by A30;

        

        thus (FD . (z39,y)) = (dq2 . [z3, y99]) by A27, A32, GRFUNC_1: 2

        .= b by A31;

      end;

        suppose l <= k;

        then A2 c= A1 by A10, A22, Th38, A20, A8;

        then

        reconsider x9 = x, y9 = y as Element of A1 by A4, A6, A8, A23;

        A1 c= Aq1 by A10, A13, Th38, A8, A9, NAT_1: 11;

        then

        reconsider x99 = x9, y99 = y9 as Element of Aq1;

        ( dom d1) = [:A1, A1:] by FUNCT_2:def 1;

        

        then (FD . (x,y)) = (d1 . [x9, y9]) by A12, GRFUNC_1: 2

        .= (d1 . (x9,y9));

        then

        consider z1,z2,z3 be Element of Aq1 such that

         A33: (dq1 . (x,z1)) = a and

         A34: (dq1 . (z2,z3)) = a and

         A35: (dq1 . (z1,z2)) = b and

         A36: (dq1 . (z3,y)) = b by A3, A7, Th37;

        reconsider z19 = z1, z29 = z2, z39 = z3 as Element of FS by A14;

        take z19, z29, z39;

        

         A37: ( dom dq1) = [:Aq1, Aq1:] by FUNCT_2:def 1;

        

        hence (FD . (x,z19)) = (dq1 . [x99, z1]) by A15, GRFUNC_1: 2

        .= a by A33;

        

        thus (FD . (z29,z39)) = (dq1 . [z2, z3]) by A15, A37, GRFUNC_1: 2

        .= a by A34;

        

        thus (FD . (z19,z29)) = (dq1 . [z1, z2]) by A15, A37, GRFUNC_1: 2

        .= b by A35;

        

        thus (FD . (z39,y)) = (dq1 . [z3, y99]) by A15, A37, GRFUNC_1: 2

        .= b by A36;

      end;

    end;

    theorem :: LATTICE5:43

    

     Th43: for S be ExtensionSeq of the carrier of L, ( BasicDF L) holds for FS be non empty set holds for FD be distance_function of FS, L holds for f be Homomorphism of L, ( EqRelLATT FS) holds for x,y be Element of FS holds for e1,e2 be Equivalence_Relation of FS, x,y be object st f = ( alpha FD) & FS = ( union the set of all ((S . i) `1 ) where i be Element of NAT ) & FD = ( union the set of all ((S . i) `2 ) where i be Element of NAT ) & e1 in the carrier of ( Image f) & e2 in the carrier of ( Image f) & [x, y] in (e1 "\/" e2) holds ex F be non empty FinSequence of FS st ( len F) = (3 + 2) & (x,y) are_joint_by (F,e1,e2)

    proof

      let S be ExtensionSeq of the carrier of L, ( BasicDF L);

      let FS be non empty set;

      let FD be distance_function of FS, L;

      let f be Homomorphism of L, ( EqRelLATT FS);

      let x,y be Element of FS;

      let e1,e2 be Equivalence_Relation of FS, x,y be object;

      assume that

       A1: f = ( alpha FD) and

       A2: FS = ( union the set of all ((S . i) `1 ) where i be Element of NAT ) & FD = ( union the set of all ((S . i) `2 ) where i be Element of NAT ) and

       A3: e1 in the carrier of ( Image f) and

       A4: e2 in the carrier of ( Image f) and

       A5: [x, y] in (e1 "\/" e2);

      

       A6: 4 in ( Seg 5);

      ( field (e1 "\/" e2)) = FS by ORDERS_1: 12;

      then

      reconsider u = x, v = y as Element of FS by A5, RELAT_1: 15;

      

       A7: 1 in ( Seg 5);

      ( Image f) = ( subrelstr ( rng f)) by YELLOW_2:def 2;

      then

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

      then

      consider a be object such that

       A9: a in ( dom f) and

       A10: e1 = (f . a) by A3, FUNCT_1:def 3;

      consider b be object such that

       A11: b in ( dom f) and

       A12: e2 = (f . b) by A4, A8, FUNCT_1:def 3;

      reconsider a, b as Element of L by A9, A11;

      reconsider a, b as Element of L;

      consider e be Equivalence_Relation of FS such that

       A13: e = (f . (a "\/" b)) and

       A14: for u,v be Element of FS holds [u, v] in e iff (FD . (u,v)) <= (a "\/" b) by A1, Def8;

      consider e19 be Equivalence_Relation of FS such that

       A15: e19 = (f . a) and

       A16: for u,v be Element of FS holds [u, v] in e19 iff (FD . (u,v)) <= a by A1, Def8;

      consider e29 be Equivalence_Relation of FS such that

       A17: e29 = (f . b) and

       A18: for u,v be Element of FS holds [u, v] in e29 iff (FD . (u,v)) <= b by A1, Def8;

      

       A19: 3 in ( Seg 5);

      e = ((f . a) "\/" (f . b)) by A13, WAYBEL_6: 2

      .= (e1 "\/" e2) by A10, A12, Th10;

      then (FD . (u,v)) <= (a "\/" b) by A5, A14;

      then

      consider z1,z2,z3 be Element of FS such that

       A20: (FD . (u,z1)) = a and

       A21: (FD . (z2,z3)) = a and

       A22: (FD . (z1,z2)) = b and

       A23: (FD . (z3,v)) = b by A2, Th42;

      defpred P[ set, object] means ($1 = 1 implies $2 = u) & ($1 = 2 implies $2 = z1) & ($1 = 3 implies $2 = z2) & ($1 = 4 implies $2 = z3) & ($1 = 5 implies $2 = v);

      

       A24: for m be Nat st m in ( Seg 5) holds ex w be object st P[m, w]

      proof

        let m be Nat;

        assume m in ( Seg 5);

        then m = 1 or ... or m = 5 by Lm3;

        per cases ;

          suppose

           A25: m = 1;

          take x;

          thus thesis by A25;

        end;

          suppose

           A26: m = 2;

          take z1;

          thus thesis by A26;

        end;

          suppose

           A27: m = 3;

          take z2;

          thus thesis by A27;

        end;

          suppose

           A28: m = 4;

          take z3;

          thus thesis by A28;

        end;

          suppose

           A29: m = 5;

          take y;

          thus thesis by A29;

        end;

      end;

      ex p be FinSequence st ( dom p) = ( Seg 5) & for k be Nat st k in ( Seg 5) holds P[k, (p . k)] from FINSEQ_1:sch 1( A24);

      then

      consider h be FinSequence such that

       A30: ( dom h) = ( Seg 5) and

       A31: for m be Nat st m in ( Seg 5) holds (m = 1 implies (h . m) = u) & (m = 2 implies (h . m) = z1) & (m = 3 implies (h . m) = z2) & (m = 4 implies (h . m) = z3) & (m = 5 implies (h . m) = v);

      

       A32: ( len h) = 5 by A30, FINSEQ_1:def 3;

      

       A33: 5 in ( Seg 5);

      

       A34: 2 in ( Seg 5);

      ( rng h) c= FS

      proof

        let w be object;

        assume w in ( rng h);

        then

        consider j be object such that

         A35: j in ( dom h) and

         A36: w = (h . j) by FUNCT_1:def 3;

        j = 1 or ... or j = 5 by A30, A35, Lm3;

        per cases ;

          suppose j = 1;

          then (h . j) = u by A31, A7;

          hence thesis by A36;

        end;

          suppose j = 2;

          then (h . j) = z1 by A31, A34;

          hence thesis by A36;

        end;

          suppose j = 3;

          then (h . j) = z2 by A31, A19;

          hence thesis by A36;

        end;

          suppose j = 4;

          then (h . j) = z3 by A31, A6;

          hence thesis by A36;

        end;

          suppose j = 5;

          then (h . j) = v by A31, A33;

          hence thesis by A36;

        end;

      end;

      then

      reconsider h as FinSequence of FS by FINSEQ_1:def 4;

      reconsider h as non empty FinSequence of FS by A30;

      

       A37: (h . 1) = x by A31, A7;

      

       A38: for j be Element of NAT st 1 <= j & j < ( len h) holds (j is odd implies [(h . j), (h . (j + 1))] in e1) & (j is even implies [(h . j), (h . (j + 1))] in e2)

      proof

        let j be Element of NAT ;

        assume 1 <= j & j < ( len h);

        then j = 1 or ... or j = 4 by A32, Lm2;

        per cases ;

          suppose

           A39: j = 1;

           [u, z1] in e19 by A16, A20;

          then [(h . 1), z1] in e19 by A31, A7;

          hence thesis by A10, A15, A31, A34, A39;

        end;

          suppose

           A40: j = 3;

           [z2, z3] in e19 by A16, A21;

          then

           A41: [(h . 3), z3] in e19 by A31, A19;

          ((2 * 1) + 1) = j by A40;

          hence thesis by A10, A15, A31, A6, A41;

        end;

          suppose

           A42: j = 2;

           [z1, z2] in e29 by A18, A22;

          then

           A43: [(h . 2), z2] in e29 by A31, A34;

          (2 * 1) = j by A42;

          hence thesis by A12, A17, A31, A19, A43;

        end;

          suppose

           A44: j = 4;

           [z3, v] in e29 by A18, A23;

          then

           A45: [(h . 4), v] in e29 by A31, A6;

          (2 * 2) = j by A44;

          hence thesis by A12, A17, A31, A33, A45;

        end;

      end;

      take h;

      thus ( len h) = (3 + 2) by A30, FINSEQ_1:def 3;

      (h . ( len h)) = (h . 5) by A30, FINSEQ_1:def 3

      .= y by A31, A33;

      hence thesis by A37, A38;

    end;

    ::$Notion-Name

    theorem :: LATTICE5:44

    ex A be non empty set, f be Homomorphism of L, ( EqRelLATT A) st f is one-to-one & ( type_of ( Image f)) <= 3

    proof

      set A = the carrier of L, D = ( BasicDF L);

      set S = the ExtensionSeq of A, D;

      set FS = ( union the set of all ((S . i) `1 ) where i be Element of NAT );

      

       A1: ((S . 0 ) `1 ) in the set of all ((S . i) `1 ) where i be Element of NAT ;

      

       A2: (S . 0 ) = [A, D] by Def20;

      A c= FS by A1, A2, ZFMISC_1: 74;

      then

      reconsider FS as non empty set;

      reconsider FD = ( union the set of all ((S . i) `2 ) where i be Element of NAT ) as distance_function of FS, L by Th41;

      ( alpha FD) is join-preserving

      proof

        set f = ( alpha FD);

        let a,b be Element of L;

        

         A3: ex_sup_of ((f .: {a, b}),( EqRelLATT FS)) by YELLOW_0: 17;

        consider e3 be Equivalence_Relation of FS such that

         A4: e3 = (f . (a "\/" b)) and

         A5: for x,y be Element of FS holds [x, y] in e3 iff (FD . (x,y)) <= (a "\/" b) by Def8;

        consider e2 be Equivalence_Relation of FS such that

         A6: e2 = (f . b) and

         A7: for x,y be Element of FS holds [x, y] in e2 iff (FD . (x,y)) <= b by Def8;

        consider e1 be Equivalence_Relation of FS such that

         A8: e1 = (f . a) and

         A9: for x,y be Element of FS holds [x, y] in e1 iff (FD . (x,y)) <= a by Def8;

        

         A10: ( field e2) = FS by ORDERS_1: 12;

        now

          let x,y be object;

          

           A11: b <= (b "\/" a) by YELLOW_0: 22;

          assume

           A12: [x, y] in e2;

          then

          reconsider x9 = x, y9 = y as Element of FS by A10, RELAT_1: 15;

          (FD . (x9,y9)) <= b by A7, A12;

          then (FD . (x9,y9)) <= (b "\/" a) by A11, ORDERS_2: 3;

          hence [x, y] in e3 by A5;

        end;

        then

         A13: e2 c= e3 by RELAT_1:def 3;

        

         A14: ( field e3) = FS by ORDERS_1: 12;

        for u,v be object holds [u, v] in e3 implies [u, v] in (e1 "\/" e2)

        proof

          let u,v be object;

          

           A15: 3 in ( Seg 5);

          assume

           A16: [u, v] in e3;

          then

          reconsider x = u, y = v as Element of FS by A14, RELAT_1: 15;

          (FD . (x,y)) <= (a "\/" b) by A5, A16;

          then

          consider z1,z2,z3 be Element of FS such that

           A17: (FD . (x,z1)) = a and

           A18: (FD . (z2,z3)) = a and

           A19: (FD . (z1,z2)) = b and

           A20: (FD . (z3,y)) = b by Th42;

          

           A21: u in FS by A14, A16, RELAT_1: 15;

          defpred P[ set, object] means ($1 = 1 implies $2 = x) & ($1 = 2 implies $2 = z1) & ($1 = 3 implies $2 = z2) & ($1 = 4 implies $2 = z3) & ($1 = 5 implies $2 = y);

          

           A22: for m be Nat st m in ( Seg 5) holds ex w be object st P[m, w]

          proof

            let m be Nat;

            assume m in ( Seg 5);

            then m = 1 or ... or m = 5 by Lm3;

            per cases ;

              suppose

               A23: m = 1;

              take x;

              thus thesis by A23;

            end;

              suppose

               A24: m = 2;

              take z1;

              thus thesis by A24;

            end;

              suppose

               A25: m = 3;

              take z2;

              thus thesis by A25;

            end;

              suppose

               A26: m = 4;

              take z3;

              thus thesis by A26;

            end;

              suppose

               A27: m = 5;

              take y;

              thus thesis by A27;

            end;

          end;

          ex p be FinSequence st ( dom p) = ( Seg 5) & for k be Nat st k in ( Seg 5) holds P[k, (p . k)] from FINSEQ_1:sch 1( A22);

          then

          consider h be FinSequence such that

           A28: ( dom h) = ( Seg 5) and

           A29: for m be Nat st m in ( Seg 5) holds (m = 1 implies (h . m) = x) & (m = 2 implies (h . m) = z1) & (m = 3 implies (h . m) = z2) & (m = 4 implies (h . m) = z3) & (m = 5 implies (h . m) = y);

          

           A30: ( len h) = 5 by A28, FINSEQ_1:def 3;

          

           A31: 5 in ( Seg 5);

          

           A32: 4 in ( Seg 5);

          

           A33: 1 in ( Seg 5);

          then

           A34: u = (h . 1) by A29;

          

           A35: 2 in ( Seg 5);

          

           A36: for j be Nat st 1 <= j & j < ( len h) holds [(h . j), (h . (j + 1))] in (e1 \/ e2)

          proof

            let j be Nat;

            assume 1 <= j & j < ( len h);

            then j = 1 or ... or j = 4 by A30, Lm2;

            per cases ;

              suppose

               A37: j = 1;

               [x, z1] in e1 by A9, A17;

              then [(h . 1), z1] in e1 by A29, A33;

              then [(h . 1), (h . 2)] in e1 by A29, A35;

              hence thesis by A37, XBOOLE_0:def 3;

            end;

              suppose

               A38: j = 3;

               [z2, z3] in e1 by A9, A18;

              then [(h . 3), z3] in e1 by A29, A15;

              then [(h . 3), (h . 4)] in e1 by A29, A32;

              hence thesis by A38, XBOOLE_0:def 3;

            end;

              suppose

               A39: j = 2;

               [z1, z2] in e2 by A7, A19;

              then [(h . 2), z2] in e2 by A29, A35;

              then [(h . 2), (h . 3)] in e2 by A29, A15;

              hence thesis by A39, XBOOLE_0:def 3;

            end;

              suppose

               A40: j = 4;

               [z3, y] in e2 by A7, A20;

              then [(h . 4), y] in e2 by A29, A32;

              then [(h . 4), (h . 5)] in e2 by A29, A31;

              hence thesis by A40, XBOOLE_0:def 3;

            end;

          end;

          v = (h . 5) by A29, A31

          .= (h . ( len h)) by A28, FINSEQ_1:def 3;

          hence thesis by A21, A30, A34, A36, EQREL_1: 28;

        end;

        then

         A41: e3 c= (e1 "\/" e2) by RELAT_1:def 3;

        

         A42: ( field e1) = FS by ORDERS_1: 12;

        now

          let x,y be object;

          

           A43: a <= (a "\/" b) by YELLOW_0: 22;

          assume

           A44: [x, y] in e1;

          then

          reconsider x9 = x, y9 = y as Element of FS by A42, RELAT_1: 15;

          (FD . (x9,y9)) <= a by A9, A44;

          then (FD . (x9,y9)) <= (a "\/" b) by A43, ORDERS_2: 3;

          hence [x, y] in e3 by A5;

        end;

        then e1 c= e3 by RELAT_1:def 3;

        then (e1 \/ e2) c= e3 by A13, XBOOLE_1: 8;

        then

         A45: (e1 "\/" e2) c= e3 by EQREL_1:def 2;

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

        

        then ( sup (f .: {a, b})) = ( sup {(f . a), (f . b)}) by FUNCT_1: 60

        .= ((f . a) "\/" (f . b)) by YELLOW_0: 41

        .= (e1 "\/" e2) by A8, A6, Th10

        .= (f . (a "\/" b)) by A4, A45, A41

        .= (f . ( sup {a, b})) by YELLOW_0: 41;

        hence thesis by A3;

      end;

      then

      reconsider f = ( alpha FD) as Homomorphism of L, ( EqRelLATT FS) by Th14;

      

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

      

       A47: ( Image f) = ( subrelstr ( rng f)) by YELLOW_2:def 2;

      

       A48: ex e be Equivalence_Relation of FS st e in the carrier of ( Image f) & e <> ( id FS)

      proof

        

         A49: {A} <> { {A}}

        proof

          assume {A} = { {A}};

          then {A} in {A} by TARSKI:def 1;

          hence contradiction;

        end;

        consider A9 be non empty set, d9 be distance_function of A9, L, Aq9 be non empty set, dq9 be distance_function of Aq9, L such that

         A50: (Aq9,dq9) is_extension_of (A9,d9) and

         A51: (S . 0 ) = [A9, d9] and

         A52: (S . ( 0 + 1)) = [Aq9, dq9] by Def20;

        A9 = A & d9 = D by A2, A51, XTUPLE_0: 1;

        then

        consider q be QuadrSeq of D such that

         A53: Aq9 = ( NextSet D) and

         A54: dq9 = ( NextDelta q) by A50;

        ( ConsecutiveSet (A, {} )) = A by Th21;

        then

        reconsider Q = ( Quadr (q, {} )) as Element of [:A, A, the carrier of L, the carrier of L:];

        

         A55: ((S . 1) `2 ) in the set of all ((S . i) `2 ) where i be Element of NAT ;

        ( succ {} ) c= ( DistEsti D) by Lm4;

        then {} in ( DistEsti D) by ORDINAL1: 21;

        then

         A56: {} in ( dom q) by Th25;

        then (q . {} ) in ( rng q) by FUNCT_1:def 3;

        then (q . {} ) in { [u, v, a9, b9] where u be Element of A, v be Element of A, a9 be Element of L, b9 be Element of L : (D . (u,v)) <= (a9 "\/" b9) } by Def13;

        then

        consider u,v be Element of A, a,b be Element of L such that

         A57: (q . {} ) = [u, v, a, b] and (D . (u,v)) <= (a "\/" b);

        consider e be Equivalence_Relation of FS such that

         A58: e = (f . b) and

         A59: for x,y be Element of FS holds [x, y] in e iff (FD . (x,y)) <= b by Def8;

        

         A60: ( Quadr (q, {} )) = [u, v, a, b] by A56, A57, Def14;

        ( [Aq9, dq9] `2 ) = ( NextDelta q) by A54;

        then

         A61: ( NextDelta q) c= FD by A55, A52, ZFMISC_1: 74;

        

         A62: { {A}} in { {A}, { {A}}, { { {A}}}} by ENUMSET1:def 1;

        then

         A63: { {A}} in (A \/ { {A}, { {A}}, { { {A}}}}) by XBOOLE_0:def 3;

        take e;

        e in ( rng f) by A46, A58, FUNCT_1:def 3;

        hence e in the carrier of ( Image f) by A47, YELLOW_0:def 15;

        

         A64: ((S . 1) `1 ) in the set of all ((S . i) `1 ) where i be Element of NAT ;

        ( [Aq9, dq9] `1 ) = ( NextSet D) by A53;

        then

         A65: ( NextSet D) c= FS by A64, A52, ZFMISC_1: 74;

        ( new_set A) = ( new_set ( ConsecutiveSet (A, {} ))) by Th21

        .= ( ConsecutiveSet (A,( succ {} ))) by Th22;

        then ( new_set A) c= ( NextSet D) by Lm4, Th29;

        then

         A66: ( new_set A) c= FS by A65;

        

         A67: { {A}} in ( new_set A) by A62, XBOOLE_0:def 3;

        

         A68: {A} in { {A}, { {A}}, { { {A}}}} by ENUMSET1:def 1;

        then {A} in (A \/ { {A}, { {A}}, { { {A}}}}) by XBOOLE_0:def 3;

        then

        reconsider W = {A}, V = { {A}} as Element of FS by A66, A67;

        

         A69: ( ConsecutiveSet (A, {} )) = A & ( ConsecutiveDelta (q, {} )) = D by Th21, Th26;

        ( ConsecutiveDelta (q,( succ {} ))) = ( new_bi_fun (( BiFun (( ConsecutiveDelta (q, {} )),( ConsecutiveSet (A, {} )),L)),( Quadr (q, {} )))) by Th27

        .= ( new_bi_fun (D,Q)) by A69, Def15;

        then ( new_bi_fun (D,Q)) c= ( NextDelta q) by Lm4, Th32;

        then

         A70: ( new_bi_fun (D,Q)) c= FD by A61;

        ( dom ( new_bi_fun (D,Q))) = [:( new_set A), ( new_set A):] & {A} in ( new_set A) by A68, FUNCT_2:def 1, XBOOLE_0:def 3;

        then [ {A}, { {A}}] in ( dom ( new_bi_fun (D,Q))) by A63, ZFMISC_1: 87;

        

        then (FD . (W,V)) = (( new_bi_fun (D,Q)) . ( {A}, { {A}})) by A70, GRFUNC_1: 2

        .= (Q `4_4 ) by Def10

        .= b by A60;

        then [ {A}, { {A}}] in e by A59;

        hence thesis by A49, RELAT_1:def 10;

      end;

      take FS, f;

      D is onto by Th40;

      then

       A71: ( rng D) = A by FUNCT_2:def 3;

      for w be object st w in A holds ex z be object st z in [:FS, FS:] & w = (FD . z)

      proof

        let w be object;

        

         A72: ((S . 0 ) `1 ) in the set of all ((S . i) `1 ) where i be Element of NAT ;

        

         A73: ((S . 0 ) `2 ) in the set of all ((S . i) `2 ) where i be Element of NAT ;

        

         A74: (S . 0 ) = [A, D] by Def20;

        

         A75: D c= FD by A73, A74, ZFMISC_1: 74;

        assume w in A;

        then

        consider z be object such that

         A76: z in [:A, A:] and

         A77: (D . z) = w by A71, FUNCT_2: 11;

        take z;

        A c= FS by A72, A74, ZFMISC_1: 74;

        then [:A, A:] c= [:FS, FS:] by ZFMISC_1: 96;

        hence z in [:FS, FS:] by A76;

        z in ( dom D) by A76, FUNCT_2:def 1;

        hence thesis by A77, A75, GRFUNC_1: 2;

      end;

      then ( rng FD) = A by FUNCT_2: 10;

      then FD is onto by FUNCT_2:def 3;

      hence f is one-to-one by Th15;

      for e1,e2 be Equivalence_Relation of FS, x,y be object st e1 in the carrier of ( Image f) & e2 in the carrier of ( Image f) & [x, y] in (e1 "\/" e2) holds ex F be non empty FinSequence of FS st ( len F) = (3 + 2) & (x,y) are_joint_by (F,e1,e2) by Th43;

      hence thesis by A48, Th13;

    end;