lattice8.miz



    begin

    definition

      let L be RelStr;

      :: LATTICE8:def1

      attr L is finitely_typed means

      : Def1: ex A be non empty set st (for e be object st e in the carrier of L holds e is Equivalence_Relation of A) & ex o be Element of NAT st for e1,e2 be Equivalence_Relation of A, x,y be object st e1 in the carrier of L & e2 in the carrier of L & [x, y] in (e1 "\/" e2) holds ex F be non empty FinSequence of A st ( len F) = o & (x,y) are_joint_by (F,e1,e2);

    end

    definition

      let L be lower-bounded LATTICE;

      let n be Element of NAT ;

      :: LATTICE8:def2

      pred L has_a_representation_of_type<= n means ex A be non trivial set, f be Homomorphism of L, ( EqRelLATT A) st f is one-to-one & ( Image f) is finitely_typed & (ex e be Equivalence_Relation of A st e in the carrier of ( Image f) & e <> ( id A)) & ( type_of ( Image f)) <= n;

    end

    registration

      cluster lower-bounded distributive finite for LATTICE;

      existence

      proof

        set L = the distributive finite LATTICE;

        take L;

        thus thesis;

      end;

    end

    

     Lm1: 1 is odd

    proof

      ((2 * 0 ) + 1) = 1;

      hence thesis;

    end;

    

     Lm2: 2 is even

    proof

      (2 * 1) = 2;

      hence thesis;

    end;

    registration

      let A be non trivial set;

      cluster non trivial finitely_typed full for non empty Sublattice of ( EqRelLATT A);

      existence

      proof

        reconsider e1 = ( nabla A), e2 = ( id A) as Element of ( EqRelLATT A) by LATTICE5: 4;

        set a = the Element of A;

        set b = the Element of (A \ {a});

        set Y = ( subrelstr {e1, e2});

        

         A1: the carrier of Y = {e1, e2} by YELLOW_0:def 15;

        e1 = [:A, A:] by EQREL_1:def 1;

        then

         A2: e2 <= e1 by LATTICE5: 6;

        

         A3: for x,y be Element of ( EqRelLATT A) st x in the carrier of Y & y in the carrier of Y & ex_inf_of ( {x, y},( EqRelLATT A)) holds ( inf {x, y}) in the carrier of Y

        proof

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

          assume that

           A4: x in the carrier of Y & y in the carrier of Y and ex_inf_of ( {x, y},( EqRelLATT A));

          per cases by A1, A4, TARSKI:def 2;

            suppose x = e1 & y = e1;

            

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

            .= e1 by YELLOW_5: 2;

            hence thesis by A1, TARSKI:def 2;

          end;

            suppose x = e1 & y = e2;

            

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

            .= e2 by A2, YELLOW_5: 10;

            hence thesis by A1, TARSKI:def 2;

          end;

            suppose x = e2 & y = e1;

            

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

            .= e2 by A2, YELLOW_5: 10;

            hence thesis by A1, TARSKI:def 2;

          end;

            suppose x = e2 & y = e2;

            

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

            .= e2 by YELLOW_5: 2;

            hence thesis by A1, TARSKI:def 2;

          end;

        end;

        

         A5: Y is finitely_typed

        proof

          take A;

          thus for e be object st e in the carrier of Y holds e is Equivalence_Relation of A by A1, TARSKI:def 2;

          take o = 3;

          thus for eq1,eq2 be Equivalence_Relation of A, x1,y1 be object st eq1 in the carrier of Y & eq2 in the carrier of Y & [x1, y1] in (eq1 "\/" eq2) holds ex F be non empty FinSequence of A st ( len F) = o & (x1,y1) are_joint_by (F,eq1,eq2)

          proof

            let eq1,eq2 be Equivalence_Relation of A;

            let x1,y1 be object;

            assume that

             A6: eq1 in the carrier of Y and

             A7: eq2 in the carrier of Y and

             A8: [x1, y1] in (eq1 "\/" eq2);

            eq1 = e2 or eq1 <> e2;

            then

            consider z be object such that

             A9: eq1 = e2 & z = x1 or eq1 <> e2 & z = y1;

            ex x2,y2 be object st [x1, y1] = [x2, y2] & x2 in A & y2 in A by A8, RELSET_1: 2;

            then x1 in A & y1 in A by XTUPLE_0: 1;

            then

            reconsider F = <*x1, z, y1*> as non empty FinSequence of A by A9, FINSEQ_2: 14;

            take F;

            per cases by A9;

              suppose

               A10: eq1 = e2 & z = x1;

              then

               A11: (F . 2) = x1 by FINSEQ_1: 45;

              

               A12: (F . 1) = x1 by FINSEQ_1: 45;

              

               A13: for i be Element of NAT st 1 <= i & i < ( len F) holds (i is odd implies [(F . i), (F . (i + 1))] in eq1) & (i is even implies [(F . i), (F . (i + 1))] in eq2)

              proof

                let i be Element of NAT ;

                assume that

                 A14: 1 <= i and

                 A15: i < ( len F);

                i < (2 + 1) by A15, FINSEQ_1: 45;

                then i <= 2 by NAT_1: 13;

                then

                 A16: i = 0 or ... or i = 2 by NAT_1: 60;

                per cases by A1, A7, A10, A14, A16, Lm1, Lm2, TARSKI:def 2;

                  suppose

                   A17: i = 1 & i is odd & eq1 = e2 & eq2 = e1;

                  ex x2,y2 be object st [x1, y1] = [x2, y2] & x2 in A & y2 in A by A8, RELSET_1: 2;

                  then x1 in A by XTUPLE_0: 1;

                  hence thesis by A12, A11, A17, EQREL_1: 5;

                end;

                  suppose

                   A18: i = 1 & i is odd & eq1 = e2 & eq2 = e2;

                  ex x2,y2 be object st [x1, y1] = [x2, y2] & x2 in A & y2 in A by A8, RELSET_1: 2;

                  then x1 in A by XTUPLE_0: 1;

                  hence thesis by A12, A11, A18, EQREL_1: 5;

                end;

                  suppose

                   A19: i = 2 & i is even & eq1 = e2 & eq2 = e1;

                  

                  then (eq1 "\/" eq2) = (e2 "\/" e1) by LATTICE5: 10

                  .= eq2 by A2, A19, YELLOW_5: 8;

                  hence thesis by A8, A11, A19, FINSEQ_1: 45;

                end;

                  suppose i = 2 & i is even & eq1 = e2 & eq2 = e2;

                  hence thesis by A8, A11, FINSEQ_1: 45;

                end;

              end;

              ( len F) = 3 & (F . 3) = y1 by FINSEQ_1: 45;

              hence thesis by A12, A13;

            end;

              suppose

               A20: eq1 <> e2 & z = y1;

              then

               A21: (F . 2) = y1 by FINSEQ_1: 45;

              

               A22: (F . 3) = y1 by FINSEQ_1: 45;

              

               A23: for i be Element of NAT st 1 <= i & i < ( len F) holds (i is odd implies [(F . i), (F . (i + 1))] in eq1) & (i is even implies [(F . i), (F . (i + 1))] in eq2)

              proof

                let i be Element of NAT ;

                assume that

                 A24: 1 <= i and

                 A25: i < ( len F);

                i < (2 + 1) by A25, FINSEQ_1: 45;

                then i <= 2 by NAT_1: 13;

                then

                 A26: i = 0 or ... or i = 2 by NAT_1: 60;

                per cases by A1, A6, A7, A20, A24, A26, Lm1, Lm2, TARSKI:def 2;

                  suppose i = 1 & i is odd & eq1 = e1 & eq2 = e1;

                  hence thesis by A8, A21, FINSEQ_1: 45;

                end;

                  suppose

                   A27: i = 1 & i is odd & eq1 = e1 & eq2 = e2;

                  

                  then (eq1 "\/" eq2) = (e1 "\/" e2) by LATTICE5: 10

                  .= eq1 by A2, A27, YELLOW_5: 8;

                  hence thesis by A8, A21, A27, FINSEQ_1: 45;

                end;

                  suppose

                   A28: i = 2 & i is even & eq1 = e1 & eq2 = e1;

                  ex x2,y2 be object st [x1, y1] = [x2, y2] & x2 in A & y2 in A by A8, RELSET_1: 2;

                  then y1 in A by XTUPLE_0: 1;

                  hence thesis by A21, A22, A28, EQREL_1: 5;

                end;

                  suppose

                   A29: i = 2 & i is even & eq1 = e1 & eq2 = e2;

                  ex x2,y2 be object st [x1, y1] = [x2, y2] & x2 in A & y2 in A by A8, RELSET_1: 2;

                  then y1 in A by XTUPLE_0: 1;

                  hence thesis by A21, A22, A29, EQREL_1: 5;

                end;

              end;

              ( len F) = 3 & (F . 1) = x1 by FINSEQ_1: 45;

              hence thesis by A22, A23;

            end;

          end;

        end;

        

         A30: for x,y be Element of ( EqRelLATT A) st x in the carrier of Y & y in the carrier of Y & ex_sup_of ( {x, y},( EqRelLATT A)) holds ( sup {x, y}) in the carrier of Y

        proof

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

          assume that

           A31: x in the carrier of Y & y in the carrier of Y and ex_sup_of ( {x, y},( EqRelLATT A));

          per cases by A1, A31, TARSKI:def 2;

            suppose x = e1 & y = e1;

            

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

            .= e1 by YELLOW_5: 1;

            hence thesis by A1, TARSKI:def 2;

          end;

            suppose x = e1 & y = e2;

            

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

            .= e1 by A2, YELLOW_5: 8;

            hence thesis by A1, TARSKI:def 2;

          end;

            suppose x = e2 & y = e1;

            

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

            .= e1 by A2, YELLOW_5: 8;

            hence thesis by A1, TARSKI:def 2;

          end;

            suppose x = e2 & y = e2;

            

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

            .= e2 by YELLOW_5: 1;

            hence thesis by A1, TARSKI:def 2;

          end;

        end;

        

         A32: a <> b by ZFMISC_1: 56;

        

         A33: Y is non trivial

        proof

          assume Y is trivial;

          then ex s be Element of Y st the carrier of Y = {s} by TEX_1:def 1;

          then ( nabla A) = ( id A) by A1, ZFMISC_1: 5;

          then [:A, A:] = ( id A) by EQREL_1:def 1;

          then [a, b] in ( id A) by ZFMISC_1:def 2;

          hence contradiction by A32, RELAT_1:def 10;

        end;

        reconsider Y as full non empty Sublattice of ( EqRelLATT A) by A3, A30, YELLOW_0:def 16, YELLOW_0:def 17;

        take Y;

        thus thesis by A33, A5;

      end;

    end

    theorem :: LATTICE8:1

    

     Th1: for A be non empty set holds for L be lower-bounded LATTICE holds for d be distance_function of A, L holds ( succ {} ) c= ( DistEsti d)

    proof

      let A be non empty set;

      let L be lower-bounded LATTICE;

      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 thesis by LATTICE5: 20, XBOOLE_1: 3;

    end;

    theorem :: LATTICE8:2

    for L be trivial Semilattice holds L is modular by STRUCT_0:def 10;

    theorem :: LATTICE8:3

    for A be non empty set holds for L be non empty Sublattice of ( EqRelLATT A) holds L is trivial or ex e be Equivalence_Relation of A st e in the carrier of L & e <> ( id A)

    proof

      let A be non empty set;

      let L be non empty Sublattice of ( EqRelLATT A);

      now

        assume

         A1: not ex e be Equivalence_Relation of A st e in the carrier of L & e <> ( id A);

        thus L is trivial

        proof

          consider x be object such that

           A2: x in the carrier of L by XBOOLE_0:def 1;

          the carrier of L c= the carrier of ( EqRelLATT A) by YELLOW_0:def 13;

          then

          reconsider e = x as Equivalence_Relation of A by A2, LATTICE5: 4;

          the carrier of L = {x}

          proof

            thus the carrier of L c= {x}

            proof

              let a be object;

              assume

               A3: a in the carrier of L;

              the carrier of L c= the carrier of ( EqRelLATT A) by YELLOW_0:def 13;

              then

              reconsider B = a as Equivalence_Relation of A by A3, LATTICE5: 4;

              B = ( id A) by A1, A3

              .= e by A1, A2;

              hence thesis by TARSKI:def 1;

            end;

            let A be object;

            assume A in {x};

            hence thesis by A2, TARSKI:def 1;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: LATTICE8:4

    for L1,L2 be lower-bounded LATTICE holds for f be Function of L1, L2 st f is infs-preserving sups-preserving holds f is meet-preserving join-preserving;

    theorem :: LATTICE8:5

    

     Th5: for L1,L2 be lower-bounded LATTICE st (L1,L2) are_isomorphic & L1 is modular holds L2 is modular

    proof

      let L1,L2 be lower-bounded LATTICE;

      assume that

       A1: (L1,L2) are_isomorphic and

       A2: L1 is modular;

      let a,b,c be Element of L2;

      consider f be Function of L1, L2 such that

       A3: f is isomorphic by A1, WAYBEL_1:def 8;

      set C = ((f " ) . c);

      set A = ((f " ) . a);

      set B = ((f " ) . b);

      

       A4: f is one-to-one & ( rng f) = the carrier of L2 by A3, WAYBEL_0: 66;

      then

       A5: b = (f . B) by FUNCT_1: 35;

      

       A6: C in ( dom f) by A4, FUNCT_1: 32;

      

       A7: A in ( dom f) & B in ( dom f) by A4, FUNCT_1: 32;

      

       A8: a = (f . A) & c = (f . C) by A4, FUNCT_1: 35;

      reconsider A, B, C as Element of L1 by A7, A6;

      assume a <= c;

      then A <= C by A3, A8, WAYBEL_0: 66;

      then

       A9: (A "\/" (B "/\" C)) = ((A "\/" B) "/\" C) by A2;

      f is infs-preserving sups-preserving by A3, WAYBEL13: 20;

      then

       A10: f is meet-preserving join-preserving;

      

      hence (a "\/" (b "/\" c)) = ((f . A) "\/" (f . (B "/\" C))) by A5, A8, WAYBEL_6: 1

      .= (f . ((A "\/" B) "/\" C)) by A10, A9, WAYBEL_6: 2

      .= ((f . (A "\/" B)) "/\" (f . C)) by A10, WAYBEL_6: 1

      .= ((a "\/" b) "/\" c) by A10, A5, A8, WAYBEL_6: 2;

    end;

    theorem :: LATTICE8:6

    

     Th6: for S be lower-bounded non empty Poset holds for T be non empty Poset holds for f be monotone Function of S, T holds ( Image f) is lower-bounded

    proof

      let S be lower-bounded non empty Poset;

      let T be non empty Poset;

      let f be monotone Function of S, T;

      thus ( Image f) is lower-bounded

      proof

        consider x be Element of S such that

         A1: x is_<=_than the carrier of S by YELLOW_0:def 4;

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

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

        then

        reconsider fx = (f . x) as Element of ( Image f) by YELLOW_0:def 15;

        take fx;

        let b be Element of ( Image f);

        b in the carrier of ( subrelstr ( rng f));

        then b in ( rng f) by YELLOW_0:def 15;

        then

        consider c be object such that

         A2: c in ( dom f) and

         A3: (f . c) = b by FUNCT_1:def 3;

        

         A4: the carrier of ( Image f) c= the carrier of T by YELLOW_0:def 13;

        assume b in the carrier of ( Image f);

        reconsider b1 = b as Element of T by A4;

        reconsider c as Element of S by A2;

        x <= c by A1;

        then (f . x) <= b1 by A3, ORDERS_3:def 5;

        hence fx <= b by YELLOW_0: 60;

      end;

    end;

    theorem :: LATTICE8:7

    

     Th7: for L be lower-bounded LATTICE holds for x,y be Element of L holds for A be non empty set holds for f be Homomorphism of L, ( EqRelLATT A) st f is one-to-one holds (( corestr f) . x) <= (( corestr f) . y) implies x <= y

    proof

      let L be lower-bounded LATTICE;

      let x,y be Element of L;

      let A be non empty set;

      let f be Homomorphism of L, ( EqRelLATT A);

      assume that

       A1: f is one-to-one and

       A2: (( corestr f) . x) <= (( corestr f) . y);

      now

        

         A3: ( corestr f) = f by WAYBEL_1: 30;

        

         A4: for x,y be Element of L holds (( corestr f) . (x "/\" y)) = ((( corestr f) . x) "/\" (( corestr f) . y))

        proof

          let x,y be Element of L;

          

          thus (( corestr f) . (x "/\" y)) = ((f . x) "/\" (f . y)) by A3, WAYBEL_6: 1

          .= ((( corestr f) . x) "/\" (( corestr f) . y)) by A3, YELLOW_0: 69;

        end;

        

         A5: ( corestr f) is one-to-one by A1, WAYBEL_1: 30;

        ((( corestr f) . y) "/\" (( corestr f) . x)) = (( corestr f) . x) by A2, YELLOW_5: 10;

        then (( corestr f) . x) = (( corestr f) . (x "/\" y)) by A4;

        then

         A6: x = (x "/\" y) by A5, WAYBEL_1:def 1;

        assume not x <= y;

        hence contradiction by A6, YELLOW_0: 25;

      end;

      hence thesis;

    end;

    begin

    theorem :: LATTICE8:8

    

     Th8: for A be non trivial set holds for L be finitely_typed full non empty Sublattice of ( EqRelLATT A) holds for e be Equivalence_Relation of A st e in the carrier of L & e <> ( id A) holds ( type_of L) <= 2 implies L is modular

    proof

      let A be non trivial set;

      let L be finitely_typed full non empty Sublattice of ( EqRelLATT A);

      let e be Equivalence_Relation of A;

      assume that

       A1: e in the carrier of L and

       A2: e <> ( id A);

      assume

       A3: ( type_of L) <= 2;

      let a,b,c be Element of L;

      

       A4: the carrier of L c= the carrier of ( EqRelLATT A) by YELLOW_0:def 13;

      reconsider b9 = b as Equivalence_Relation of A by A4, LATTICE5: 4;

      reconsider b99 = b9 as Element of ( EqRelLATT A) by A4;

      reconsider a9 = a as Equivalence_Relation of A by A4, LATTICE5: 4;

      reconsider c9 = c as Equivalence_Relation of A by A4, LATTICE5: 4;

      reconsider c99 = c9 as Element of ( EqRelLATT A) by A4;

      reconsider a99 = a9 as Element of ( EqRelLATT A) by A4;

      

       A5: ((a99 "\/" b99) "/\" c99) = ((a99 "\/" b99) /\ c9) by LATTICE5: 8

      .= ((a9 "\/" b9) /\ c9) by LATTICE5: 10;

      assume

       A6: a <= c;

      then a99 <= c99 by YELLOW_0: 59;

      then

       A7: a9 c= c9 by LATTICE5: 6;

      

       A8: (a99 "\/" (b99 "/\" c99)) <= ((a99 "\/" b99) "/\" c99) by A6, YELLOW11: 8, YELLOW_0: 59;

      

       A9: (b9 /\ c9) = (b99 "/\" c99) by LATTICE5: 8;

      then (a9 "\/" (b9 /\ c9)) = (a99 "\/" (b99 "/\" c99)) by LATTICE5: 10;

      then

       A10: (a9 "\/" (b9 /\ c9)) c= ((a9 "\/" b9) /\ c9) by A8, A5, LATTICE5: 6;

      consider AA be non empty set such that

       A11: for e be object st e in the carrier of L holds e is Equivalence_Relation of AA and

       A12: ex i be Element of NAT st for e1,e2 be Equivalence_Relation of AA, x,y be object st e1 in the carrier of L & e2 in the carrier of L & [x, y] in (e1 "\/" e2) holds ex F be non empty FinSequence of AA st ( len F) = i & (x,y) are_joint_by (F,e1,e2) by Def1;

      e is Equivalence_Relation of AA by A1, A11;

      then

       A13: ( field e) = A & ( field e) = AA by EQREL_1: 9;

      

       A14: ((a9 "\/" b9) /\ c9) c= (a9 "\/" (b9 /\ c9))

      proof

        let x,y be Element of A;

        assume

         A15: [x, y] in ((a9 "\/" b9) /\ c9);

        then

         A16: [x, y] in (a9 "\/" b9) by XBOOLE_0:def 4;

        

         A17: [x, y] in c9 by A15, XBOOLE_0:def 4;

        ( type_of L) = 0 or ... or ( type_of L) = 2 by A3, NAT_1: 60;

        per cases ;

          suppose ( type_of L) = 2;

          then

          consider F be non empty FinSequence of A such that

           A18: ( len F) = (2 + 2) and

           A19: (x,y) are_joint_by (F,a9,b9) by A1, A2, A12, A13, A16, LATTICE5:def 4;

          

           A20: (F . 4) = y by A18, A19;

          consider l be Element of NAT such that

           A21: l = 1;

          ((2 * l) + 1) = 3 by A21;

          then

           A22: [(F . 3), (F . (3 + 1))] in a9 by A18, A19;

          consider k be Element of NAT such that

           A23: k = 1;

          (2 * k) = 2 by A23;

          then

           A24: [(F . 2), (F . (2 + 1))] in b9 by A18, A19;

          

           A25: (F . 1) = x by A19;

          reconsider BC = (b9 /\ c9) as Element of ( EqRelLATT A) by A9;

          set z1 = (F . 2);

          set z2 = (F . 3);

          consider j be Element of NAT such that

           A26: j = 0 ;

          ((2 * j) + 1) = 1 by A26;

          then

           A27: [(F . 1), (F . (1 + 1))] in a9 by A18, A19;

          

           A28: (a9 "\/" (b9 /\ c9)) = (a99 "\/" BC) by LATTICE5: 10;

          BC <= (BC "\/" a99) by YELLOW_0: 22;

          then

           A29: (b9 /\ c9) c= (a9 "\/" (b9 /\ c9)) by A28, LATTICE5: 6;

          a99 <= (a99 "\/" BC) by YELLOW_0: 22;

          then

           A30: a9 c= (a9 "\/" (b9 /\ c9)) by A28, LATTICE5: 6;

           [y, x] in c9 by A17, EQREL_1: 6;

          then [z2, x] in c9 by A7, A20, A22, EQREL_1: 7;

          then [z2, z1] in c9 by A7, A25, A27, EQREL_1: 7;

          then [z1, z2] in c9 by EQREL_1: 6;

          then [z1, z2] in (b9 /\ c9) by A24, XBOOLE_0:def 4;

          then [x, z2] in (a9 "\/" (b9 /\ c9)) by A25, A27, A30, A29, EQREL_1: 7;

          hence thesis by A20, A22, A30, EQREL_1: 7;

        end;

          suppose ( type_of L) = 1;

          then

          consider F be non empty FinSequence of A such that

           A31: ( len F) = (1 + 2) and

           A32: (x,y) are_joint_by (F,a9,b9) by A1, A2, A12, A13, A16, LATTICE5:def 4;

          set z1 = (F . 2);

          consider k be Element of NAT such that

           A33: k = 1;

          reconsider BC = (b9 /\ c9) as Element of ( EqRelLATT A) by A9;

          consider j be Element of NAT such that

           A34: j = 0 ;

          ((2 * j) + 1) = 1 by A34;

          then

           A35: [(F . 1), (F . (1 + 1))] in a9 by A31, A32;

          (2 * k) = 2 by A33;

          then

           A36: [(F . 2), (F . (2 + 1))] in b9 by A31, A32;

          

           A37: (a9 "\/" (b9 /\ c9)) = (a99 "\/" BC) by LATTICE5: 10;

          

           A38: [x, y] in c9 by A15, XBOOLE_0:def 4;

          

           A39: (F . 1) = x by A32;

          then [z1, x] in c9 by A7, A35, EQREL_1: 6;

          then

           A40: [z1, y] in c9 by A38, EQREL_1: 7;

          BC <= (BC "\/" a99) by YELLOW_0: 22;

          then

           A41: (b9 /\ c9) c= (a9 "\/" (b9 /\ c9)) by A37, LATTICE5: 6;

          a99 <= (a99 "\/" BC) by YELLOW_0: 22;

          then

           A42: a9 c= (a9 "\/" (b9 /\ c9)) by A37, LATTICE5: 6;

          (F . 3) = y by A31, A32;

          then [z1, y] in (b9 /\ c9) by A36, A40, XBOOLE_0:def 4;

          hence thesis by A39, A35, A42, A41, EQREL_1: 7;

        end;

          suppose ( type_of L) = 0 ;

          then

          consider F be non empty FinSequence of A such that

           A43: ( len F) = ( 0 + 2) & (x,y) are_joint_by (F,a9,b9) by A1, A2, A12, A13, A16, LATTICE5:def 4;

          reconsider BC = (b9 /\ c9) as Element of ( EqRelLATT A) by A9;

          consider j be Element of NAT such that

           A44: j = 0 ;

          ((2 * j) + 1) = 1 by A44;

          then

           A45: [(F . 1), (F . (1 + 1))] in a9 by A43;

          a99 <= (a99 "\/" BC) & (a9 "\/" (b9 /\ c9)) = (a99 "\/" BC) by LATTICE5: 10, YELLOW_0: 22;

          then

           A46: a9 c= (a9 "\/" (b9 /\ c9)) by LATTICE5: 6;

          (F . 1) = x & (F . 2) = y by A43;

          hence thesis by A45, A46;

        end;

      end;

      (a99 "\/" b99) = (a "\/" b) by YELLOW_0: 70;

      

      then

       A47: ((a "\/" b) "/\" c) = ((a99 "\/" b99) "/\" c99) by YELLOW_0: 69

      .= ((a99 "\/" b99) /\ c9) by LATTICE5: 8

      .= ((a9 "\/" b9) /\ c9) by LATTICE5: 10;

      

       A48: (b99 "/\" c99) = (b "/\" c) by YELLOW_0: 69;

      (a9 "\/" (b9 /\ c9)) = (a99 "\/" (b99 "/\" c99)) by A9, LATTICE5: 10

      .= (a "\/" (b "/\" c)) by A48, YELLOW_0: 70;

      hence thesis by A10, A14, A47;

    end;

    theorem :: LATTICE8:9

    

     Th9: for L be lower-bounded LATTICE holds L has_a_representation_of_type<= 2 implies L is modular

    proof

      let L be lower-bounded LATTICE;

      assume L has_a_representation_of_type<= 2;

      then

      consider A be non trivial set, f be Homomorphism of L, ( EqRelLATT A) such that

       A1: f is one-to-one and

       A2: (( Image f) is finitely_typed & ex e be Equivalence_Relation of A st e in the carrier of ( Image f) & e <> ( id A)) & ( type_of ( Image f)) <= 2;

      

       A3: ( rng ( corestr f)) = the carrier of ( Image f) & for x,y be Element of L holds x <= y implies (( corestr f) . x) <= (( corestr f) . y) by FUNCT_2:def 3, WAYBEL_1:def 2;

      ( corestr f) is one-to-one & for x,y be Element of L holds (( corestr f) . x) <= (( corestr f) . y) implies x <= y by A1, Th7, WAYBEL_1: 30;

      then ( corestr f) is isomorphic by A3, WAYBEL_0: 66;

      then

       A4: (L,( Image f)) are_isomorphic by WAYBEL_1:def 8;

      

       A5: ( Image f) is lower-bounded LATTICE by Th6;

      ( Image f) is modular by A2, Th8;

      hence thesis by A5, A4, Th5, WAYBEL_1: 6;

    end;

    definition

      let A be set;

      :: LATTICE8:def3

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

      correctness ;

    end

    registration

      let A be set;

      cluster ( new_set2 A) -> non empty;

      coherence ;

    end

    definition

      let A be non empty set;

      let L be lower-bounded LATTICE;

      let d be BiFunction of A, L;

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

      :: LATTICE8:def4

      func new_bi_fun2 (d,q) -> BiFunction of ( new_set2 A), L means

      : Def4: (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}})) = (((d . ((q `1_4 ),(q `2_4 ))) "\/" (q `3_4 )) "/\" (q `4_4 )) & (it . ( { {A}}, {A})) = (((d . ((q `1_4 ),(q `2_4 ))) "\/" (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 `2_4 ))) "\/" (q `3_4 )) & (it . ( { {A}},u)) = ((d . (u,(q `2_4 ))) "\/" (q `3_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_set2 A), Element of ( new_set2 A), set] means ($1 in A & $2 in A implies $3 = (d . ($1,$2))) & ($1 = {A} & $2 = { {A}} or $2 = {A} & $1 = { {A}} implies $3 = (((d . (x,y)) "\/" a) "/\" b)) & (($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,y)) "\/" a)) & ($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,y)) "\/" a));

         { {A}} in { {A}, { {A}}} by TARSKI:def 2;

        then

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

        

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

        proof

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

          

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

          

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

          

           A5: (p = {A} or p = { {A}}) & p = q iff 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} & {A} in { {A}} by TARSKI:def 1;

            assume { {A}} in A;

            hence contradiction by A9, XREGULAR: 7;

          end;

          per cases by A3, A4, A5, TARSKI:def 2;

            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, A8;

          end;

            suppose

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

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

            thus thesis by A7, A8, A10, TARSKI:def 1;

          end;

            suppose

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

            take ( Bottom L);

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

          end;

            suppose

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

            then

            reconsider p9 = p as Element of A;

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

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

          end;

            suppose

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

            then

            reconsider p9 = p as Element of A;

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

            thus thesis by A7, A8, A13, TARSKI:def 1;

          end;

            suppose

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

            then

            reconsider q9 = q as Element of A;

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

            thus thesis by A7, A8, A14, TARSKI:def 1;

          end;

            suppose

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

            then

            reconsider q9 = q as Element of A;

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

            thus thesis by A7, A8, A15, TARSKI:def 1;

          end;

        end;

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

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

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

         {A} in { {A}, { {A}}} by TARSKI:def 2;

        then

         A17: {A} in ( new_set2 A) by XBOOLE_0:def 3;

        

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

        proof

          let u be Element of A;

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

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

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

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

          hence thesis;

        end;

        take f;

        

         A19: 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_set2 A) by XBOOLE_0:def 3;

          

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

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

        end;

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

        proof

          let u be Element of A;

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

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

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

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

          hence thesis;

        end;

        hence thesis by A17, A1, A16, A19, A18;

      end;

      uniqueness

      proof

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

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

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

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

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

         A23: (f1 . ( {A}, { {A}})) = (((d . ((q `1_4 ),(q `2_4 ))) "\/" (q `3_4 )) "/\" (q `4_4 )) and

         A24: (f1 . ( { {A}}, {A})) = (((d . ((q `1_4 ),(q `2_4 ))) "\/" (q `3_4 )) "/\" (q `4_4 )) and

         A25: for u be Element of A holds (f1 . (u, {A})) = ((d . (u,(q `1_4 ))) "\/" (q `3_4 )) & (f1 . ( {A},u)) = ((d . (u,(q `1_4 ))) "\/" (q `3_4 )) & (f1 . (u, { {A}})) = ((d . (u,(q `2_4 ))) "\/" (q `3_4 )) & (f1 . ( { {A}},u)) = ((d . (u,(q `2_4 ))) "\/" (q `3_4 )) and

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

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

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

         A29: (f2 . ( {A}, { {A}})) = (((d . ((q `1_4 ),(q `2_4 ))) "\/" (q `3_4 )) "/\" (q `4_4 )) and

         A30: (f2 . ( { {A}}, {A})) = (((d . ((q `1_4 ),(q `2_4 ))) "\/" (q `3_4 )) "/\" (q `4_4 )) and

         A31: for u be Element of A holds (f2 . (u, {A})) = ((d . (u,(q `1_4 ))) "\/" (q `3_4 )) & (f2 . ( {A},u)) = ((d . (u,(q `1_4 ))) "\/" (q `3_4 )) & (f2 . (u, { {A}})) = ((d . (u,(q `2_4 ))) "\/" (q `3_4 )) & (f2 . ( { {A}},u)) = ((d . (u,(q `2_4 ))) "\/" (q `3_4 ));

        now

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

          

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

          

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

          per cases by A32, A33, TARSKI:def 2;

            suppose

             A34: p in A & q in A;

            

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

            .= (f2 . (p,q)) by A26, A34;

          end;

            suppose

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

            then

            reconsider p9 = p as Element of A;

            

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

            .= (f2 . (p,q)) by A31, A35;

          end;

            suppose

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

            then

            reconsider p9 = p as Element of A;

            

            thus (f1 . (p,q)) = ((d . (p9,y)) "\/" a) by A25, A36

            .= (f2 . (p,q)) by A31, A36;

          end;

            suppose

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

            then

            reconsider q9 = q as Element of A;

            

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

            .= (f2 . (p,q)) by A31, A37;

          end;

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

            hence (f1 . (p,q)) = (f2 . (p,q)) by A21, A27;

          end;

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

            hence (f1 . (p,q)) = (f2 . (p,q)) by A23, A29;

          end;

            suppose

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

            then

            reconsider q9 = q as Element of A;

            

            thus (f1 . (p,q)) = ((d . (q9,y)) "\/" a) by A25, A38

            .= (f2 . (p,q)) by A31, A38;

          end;

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

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

          end;

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

            hence (f1 . (p,q)) = (f2 . (p,q)) by A22, A28;

          end;

        end;

        hence f1 = f2;

      end;

    end

    theorem :: LATTICE8:10

    

     Th10: for A be non empty set holds for L be lower-bounded LATTICE holds 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_fun2 (d,q)) is zeroed

    proof

      let A be non empty set;

      let L be lower-bounded LATTICE;

      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_fun2 (d,q));

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

      proof

        let u be Element of ( new_set2 A);

        

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

        per cases by A2, TARSKI:def 2;

          suppose u in A;

          then

          reconsider u9 = u as Element of A;

          

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

          .= ( Bottom L) by A1;

        end;

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

          hence thesis by Def4;

        end;

      end;

      hence thesis;

    end;

    theorem :: LATTICE8:11

    

     Th11: for A be non empty set holds for L be lower-bounded LATTICE holds 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_fun2 (d,q)) is symmetric

    proof

      let A be non empty set;

      let L be lower-bounded LATTICE;

      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_fun2 (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_set2 A);

      

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

      

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

      per cases by A2, A3, TARSKI:def 2;

        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 Def4

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

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

      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, Def4

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

      end;

        suppose

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

        then

        reconsider p9 = p as Element of A;

        

        thus (f . (p,q)) = ((d . (p9,y)) "\/" a) by A5, Def4

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

      end;

        suppose

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

        then

        reconsider q9 = q as Element of A;

        

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

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

      end;

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

        hence thesis;

      end;

        suppose

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

        

        hence (f . (p,q)) = (((d . (x,y)) "\/" a) "/\" b) by Def4

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

      end;

        suppose

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

        then

        reconsider q9 = q as Element of A;

        

        thus (f . (p,q)) = ((d . (q9,y)) "\/" a) by A8, Def4

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

      end;

        suppose

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

        

        hence (f . (p,q)) = (((d . (x,y)) "\/" a) "/\" b) by Def4

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

      end;

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

        hence thesis;

      end;

    end;

    theorem :: LATTICE8:12

    

     Th12: for A be non empty set holds for L be lower-bounded LATTICE st L is modular holds 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_fun2 (d,q)) is u.t.i.

    proof

      let A be non empty set;

      let L be lower-bounded LATTICE;

      assume

       A1: L is modular;

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

      let d be BiFunction of A, L;

      assume that

       A2: d is symmetric and

       A3: d is u.t.i.;

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

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

      reconsider a, b as Element of L;

      

       A4: for p,q,u be Element of ( new_set2 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_set2 A);

        assume

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

        per cases by A5, TARSKI:def 2;

          suppose

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

          then

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

          

           A7: (f . (p,q)) = (d . (p9,q9)) by Def4;

          (d . (p9,x)) <= ((d . (p9,q9)) "\/" (d . (q9,x))) by A3;

          then

           A8: ((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 A6, Def4;

          hence thesis by A7, A8, LATTICE3: 14;

        end;

          suppose

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

          then

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

          

           A10: (f . (p,q)) = (d . (p9,q9)) by Def4;

          (d . (p9,y)) <= ((d . (p9,q9)) "\/" (d . (q9,y))) by A3;

          then

           A11: ((d . (p9,y)) "\/" a) <= (((d . (p9,q9)) "\/" (d . (q9,y))) "\/" a) by WAYBEL_1: 2;

          (f . (p,u)) = ((d . (p9,y)) "\/" a) & (f . (q,u)) = ((d . (q9,y)) "\/" a) by A9, Def4;

          hence thesis by A10, A11, LATTICE3: 14;

        end;

      end;

      assume

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

      

       A13: for p,q,u be Element of ( new_set2 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_set2 A);

        assume

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

        per cases by A14, TARSKI:def 2;

          suppose

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

          

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

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

          hence thesis by A15;

        end;

          suppose

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

          then

          reconsider p9 = p as Element of A;

          a <= (a "\/" (d . (x,y))) by YELLOW_0: 22;

          then

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

          (d . (p9,y)) <= ((d . (p9,x)) "\/" (d . (x,y))) by A3;

          then

           A18: ((d . (p9,y)) "\/" a) <= (((d . (p9,x)) "\/" (d . (x,y))) "\/" a) by YELLOW_5: 7;

          a <= a;

          then ((d . (x,y)) "\/" a) <= ((a "\/" b) "\/" a) by A12, YELLOW_3: 3;

          then (((d . (x,y)) "\/" a) "/\" ((d . (x,y)) "\/" a)) <= (((d . (x,y)) "\/" a) "/\" ((a "\/" b) "\/" a)) by YELLOW_5: 6;

          then

           A19: ((d . (x,y)) "\/" a) = (((d . (x,y)) "\/" a) "/\" ((d . (x,y)) "\/" a)) & ((d . (p9,x)) "\/" (((d . (x,y)) "\/" a) "/\" ((d . (x,y)) "\/" a))) <= ((d . (p9,x)) "\/" (((d . (x,y)) "\/" a) "/\" ((a "\/" b) "\/" a))) by WAYBEL_1: 2, YELLOW_5: 2;

          (f . (p,q)) = ((d . (p9,x)) "\/" a) & (f . (q,u)) = (((d . (x,y)) "\/" a) "/\" b) by A16, Def4;

          

          then ((f . (p,q)) "\/" (f . (q,u))) = ((d . (p9,x)) "\/" ((a "\/" b) "/\" (a "\/" (d . (x,y))))) by A17, LATTICE3: 14

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

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

          then (((d . (p9,x)) "\/" (d . (x,y))) "\/" a) <= ((f . (p,q)) "\/" (f . (q,u))) by A19, LATTICE3: 14;

          then ((d . (p9,y)) "\/" a) <= ((f . (p,q)) "\/" (f . (q,u))) by A18, ORDERS_2: 3;

          hence thesis by A16, Def4;

        end;

          suppose

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

          then

          reconsider p9 = p as Element of A;

          a <= (a "\/" (d . (x,y))) by YELLOW_0: 22;

          then

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

          a <= a;

          then ((d . (x,y)) "\/" a) <= ((a "\/" b) "\/" a) by A12, YELLOW_3: 3;

          then (((d . (x,y)) "\/" a) "/\" ((d . (x,y)) "\/" a)) <= (((d . (x,y)) "\/" a) "/\" ((a "\/" b) "\/" a)) by YELLOW_5: 6;

          then

           A22: ((d . (x,y)) "\/" a) = (((d . (x,y)) "\/" a) "/\" ((d . (x,y)) "\/" a)) & ((d . (p9,y)) "\/" (((d . (x,y)) "\/" a) "/\" ((d . (x,y)) "\/" a))) <= ((d . (p9,y)) "\/" (((d . (x,y)) "\/" a) "/\" ((a "\/" b) "\/" a))) by WAYBEL_1: 2, YELLOW_5: 2;

          (d . (y,x)) = (d . (x,y)) by A2;

          then (d . (p9,x)) <= ((d . (p9,y)) "\/" (d . (x,y))) by A3;

          then

           A23: ((d . (p9,x)) "\/" a) <= (((d . (p9,y)) "\/" (d . (x,y))) "\/" a) by YELLOW_5: 7;

          (f . (p,q)) = ((d . (p9,y)) "\/" a) & (f . (q,u)) = (((d . (x,y)) "\/" a) "/\" b) by A20, Def4;

          

          then ((f . (p,q)) "\/" (f . (q,u))) = ((d . (p9,y)) "\/" ((a "\/" b) "/\" (a "\/" (d . (x,y))))) by A21, LATTICE3: 14

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

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

          then (((d . (p9,y)) "\/" (d . (x,y))) "\/" a) <= ((f . (p,q)) "\/" (f . (q,u))) by A22, LATTICE3: 14;

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

          hence thesis by A20, Def4;

        end;

          suppose

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

          

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

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

          hence thesis by A24;

        end;

      end;

      

       A25: for p,q,u be Element of ( new_set2 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_set2 A);

        assume

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

        per cases by A26, TARSKI:def 2;

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

          then (f . (p,u)) = ( Bottom L) by Def4;

          hence thesis by YELLOW_0: 44;

        end;

          suppose

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

          then

          reconsider q9 = q as Element of A;

          (d . (q9,x)) = (d . (x,q9)) by A2;

          then

           A28: (d . (x,y)) <= ((d . (q9,x)) "\/" (d . (q9,y))) by A3;

          (f . (p,q)) = ((d . (q9,x)) "\/" a) by A27, Def4;

          

          then ((f . (p,q)) "\/" (f . (q,u))) = (((d . (q9,x)) "\/" a) "\/" ((d . (q9,y)) "\/" a)) by A27, Def4

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

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

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

          .= (((d . (q9,x)) "\/" (d . (q9,y))) "\/" a) by YELLOW_5: 1;

          then

           A29: ((d . (x,y)) "\/" a) <= ((f . (p,q)) "\/" (f . (q,u))) by A28, YELLOW_5: 7;

          

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

          (f . (p,u)) = (((d . (x,y)) "\/" a) "/\" b) by A27, Def4;

          hence thesis by A29, A30, ORDERS_2: 3;

        end;

          suppose

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

          then

          reconsider q9 = q as Element of A;

          (d . (q9,x)) = (d . (x,q9)) by A2;

          then

           A32: (d . (x,y)) <= ((d . (q9,x)) "\/" (d . (q9,y))) by A3;

          (f . (p,q)) = ((d . (q9,y)) "\/" a) by A31, Def4;

          

          then ((f . (p,q)) "\/" (f . (q,u))) = (((d . (q9,x)) "\/" a) "\/" ((d . (q9,y)) "\/" a)) by A31, Def4

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

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

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

          .= (((d . (q9,x)) "\/" (d . (q9,y))) "\/" a) by YELLOW_5: 1;

          then

           A33: ((d . (x,y)) "\/" a) <= ((f . (p,q)) "\/" (f . (q,u))) by A32, YELLOW_5: 7;

          

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

          (f . (p,u)) = (((d . (x,y)) "\/" a) "/\" b) by A31, Def4;

          hence thesis by A33, A34, ORDERS_2: 3;

        end;

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

          then (f . (p,u)) = ( Bottom L) by Def4;

          hence thesis by YELLOW_0: 44;

        end;

      end;

      

       A35: for p,q,u be Element of ( new_set2 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_set2 A);

        assume

         A36: p in B & q in B & u in B;

        per cases by A36, TARSKI:def 2;

          suppose

           A37: p = {A} & q = {A} & u = {A};

          ( Bottom L) <= ((f . (p,q)) "\/" (f . (q,u))) by YELLOW_0: 44;

          hence thesis by A37, Def4;

        end;

          suppose

           A38: p = {A} & q = {A} & u = { {A}};

          

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

          .= (( Bottom L) "\/" (((d . (x,y)) "\/" a) "/\" b)) by A38, Def4

          .= (((d . (x,y)) "\/" a) "/\" b) by WAYBEL_1: 3;

          hence thesis by A38, Def4;

        end;

          suppose

           A39: p = {A} & q = { {A}} & u = {A};

          ( Bottom L) <= ((f . (p,q)) "\/" (f . (q,u))) by YELLOW_0: 44;

          hence thesis by A39, Def4;

        end;

          suppose

           A40: p = {A} & q = { {A}} & u = { {A}};

          

          then ((f . (p,q)) "\/" (f . (q,u))) = ((((d . (x,y)) "\/" a) "/\" b) "\/" (f . (q,u))) by Def4

          .= (( Bottom L) "\/" (((d . (x,y)) "\/" a) "/\" b)) by A40, Def4

          .= (((d . (x,y)) "\/" a) "/\" b) by WAYBEL_1: 3;

          hence thesis by A40, Def4;

        end;

          suppose

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

          

          then ((f . (p,q)) "\/" (f . (q,u))) = ((((d . (x,y)) "\/" a) "/\" b) "\/" (f . (q,u))) by Def4

          .= (( Bottom L) "\/" (((d . (x,y)) "\/" a) "/\" b)) by A41, Def4

          .= (((d . (x,y)) "\/" a) "/\" b) by WAYBEL_1: 3

          .= (f . (p,q)) by A41, Def4;

          hence thesis by A41;

        end;

          suppose

           A42: p = { {A}} & q = {A} & u = { {A}};

          ( Bottom L) <= ((f . (p,q)) "\/" (f . (q,u))) by YELLOW_0: 44;

          hence thesis by A42, Def4;

        end;

          suppose

           A43: p = { {A}} & q = { {A}} & u = {A};

          

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

          .= (( Bottom L) "\/" (((d . (x,y)) "\/" a) "/\" b)) by A43, Def4

          .= (((d . (x,y)) "\/" a) "/\" b) by WAYBEL_1: 3;

          hence thesis by A43, Def4;

        end;

          suppose

           A44: p = { {A}} & q = { {A}} & u = { {A}};

          ( Bottom L) <= ((f . (p,q)) "\/" (f . (q,u))) by YELLOW_0: 44;

          hence thesis by A44, Def4;

        end;

      end;

      

       A45: for p,q,u be Element of ( new_set2 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_set2 A);

        assume

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

        per cases by A46, TARSKI:def 2;

          suppose

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

          

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

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

          hence thesis;

        end;

          suppose

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

          then

          reconsider u9 = u as Element of A;

          a <= (a "\/" (d . (x,y))) by YELLOW_0: 22;

          then

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

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

          then

           A50: ((d . (u9,y)) "\/" a) <= (((d . (u9,x)) "\/" (d . (x,y))) "\/" a) by YELLOW_5: 7;

          a <= a;

          then ((d . (x,y)) "\/" a) <= ((a "\/" b) "\/" a) by A12, YELLOW_3: 3;

          then (((d . (x,y)) "\/" a) "/\" ((d . (x,y)) "\/" a)) <= (((d . (x,y)) "\/" a) "/\" ((a "\/" b) "\/" a)) by YELLOW_5: 6;

          then

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

          (f . (p,q)) = (((d . (x,y)) "\/" a) "/\" b) & (f . (q,u)) = ((d . (u9,x)) "\/" a) by A48, Def4;

          

          then ((f . (p,q)) "\/" (f . (q,u))) = ((d . (u9,x)) "\/" ((a "\/" b) "/\" (a "\/" (d . (x,y))))) by A49, LATTICE3: 14

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

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

          then (((d . (u9,x)) "\/" (d . (x,y))) "\/" a) <= ((f . (p,q)) "\/" (f . (q,u))) by A51, LATTICE3: 14;

          then ((d . (u9,y)) "\/" a) <= ((f . (p,q)) "\/" (f . (q,u))) by A50, ORDERS_2: 3;

          hence thesis by A48, Def4;

        end;

          suppose

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

          then

          reconsider u9 = u as Element of A;

          a <= (a "\/" (d . (x,y))) by YELLOW_0: 22;

          then

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

          a <= a;

          then ((d . (x,y)) "\/" a) <= ((a "\/" b) "\/" a) by A12, YELLOW_3: 3;

          then (((d . (x,y)) "\/" a) "/\" ((d . (x,y)) "\/" a)) <= (((d . (x,y)) "\/" a) "/\" ((a "\/" b) "\/" a)) by YELLOW_5: 6;

          then

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

          (d . (y,x)) = (d . (x,y)) by A2;

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

          then

           A55: ((d . (u9,x)) "\/" a) <= (((d . (u9,y)) "\/" (d . (x,y))) "\/" a) by YELLOW_5: 7;

          (f . (p,q)) = (((d . (x,y)) "\/" a) "/\" b) & (f . (q,u)) = ((d . (u9,y)) "\/" a) by A52, Def4;

          

          then ((f . (p,q)) "\/" (f . (q,u))) = ((d . (u9,y)) "\/" ((a "\/" b) "/\" (a "\/" (d . (x,y))))) by A53, LATTICE3: 14

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

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

          then (((d . (u9,y)) "\/" (d . (x,y))) "\/" a) <= ((f . (p,q)) "\/" (f . (q,u))) by A54, LATTICE3: 14;

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

          hence thesis by A52, Def4;

        end;

          suppose

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

          

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

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

          hence thesis;

        end;

      end;

      

       A57: for p,q,u be Element of ( new_set2 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_set2 A);

        assume that

         A58: p in B and

         A59: q in A & u in A;

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

        per cases by A58, A59, TARSKI:def 2;

          suppose

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

          (d . (u9,x)) <= ((d . (u9,q9)) "\/" (d . (q9,x))) by A3;

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

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

          then

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

          

           A62: (f . (q,u)) = (d . (q9,u9)) by Def4;

          (f . (p,q)) = ((d . (q9,x)) "\/" a) by A60, Def4;

          hence thesis by A60, A62, A61, Def4;

        end;

          suppose

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

          (d . (u9,y)) <= ((d . (u9,q9)) "\/" (d . (q9,y))) by A3;

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

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

          then

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

          

           A65: (f . (q,u)) = (d . (q9,u9)) by Def4;

          (f . (p,q)) = ((d . (q9,y)) "\/" a) by A63, Def4;

          hence thesis by A63, A65, A64, Def4;

        end;

      end;

      

       A66: for p,q,u be Element of ( new_set2 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_set2 A);

        assume

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

        per cases by A67, TARSKI:def 2;

          suppose

           A68: 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 A3;

          then

           A69: ((d . (p9,x)) "\/" (d . (u9,x))) <= (((d . (p9,x)) "\/" (d . (u9,x))) "\/" a) & (d . (p9,u9)) <= ((d . (p9,x)) "\/" (d . (u9,x))) by A2, 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

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

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

          hence thesis by A70, Def4;

        end;

          suppose

           A71: 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 A3;

          then

           A72: ((d . (p9,y)) "\/" (d . (u9,y))) <= (((d . (p9,y)) "\/" (d . (u9,y))) "\/" a) & (d . (p9,u9)) <= ((d . (p9,y)) "\/" (d . (u9,y))) by A2, YELLOW_0: 22;

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

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

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

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

          then

           A73: (d . (p9,u9)) <= (((d . (p9,y)) "\/" a) "\/" ((d . (u9,y)) "\/" a)) by A72, ORDERS_2: 3;

          (f . (p,q)) = ((d . (p9,y)) "\/" a) & (f . (q,u)) = ((d . (u9,y)) "\/" a) by A71, Def4;

          hence thesis by A73, Def4;

        end;

      end;

      

       A74: for p,q,u be Element of ( new_set2 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_set2 A);

        assume p in A & q in A & u in A;

        then

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

        

         A75: (f . (q,u)) = (d . (q9,u9)) by Def4;

        (f . (p,u)) = (d . (p9,u9)) & (f . (p,q)) = (d . (p9,q9)) by Def4;

        hence thesis by A3, A75;

      end;

      for p,q,u be Element of ( new_set2 A) holds (f . (p,u)) <= ((f . (p,q)) "\/" (f . (q,u)))

      proof

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

        per cases by XBOOLE_0:def 3;

          suppose p in A & q in A & u in A;

          hence thesis by A74;

        end;

          suppose p in A & q in A & u in B;

          hence thesis by A4;

        end;

          suppose p in A & q in B & u in A;

          hence thesis by A66;

        end;

          suppose p in A & q in B & u in B;

          hence thesis by A13;

        end;

          suppose p in B & q in A & u in A;

          hence thesis by A57;

        end;

          suppose p in B & q in A & u in B;

          hence thesis by A25;

        end;

          suppose p in B & q in B & u in A;

          hence thesis by A45;

        end;

          suppose p in B & q in B & u in B;

          hence thesis by A35;

        end;

      end;

      hence thesis;

    end;

    theorem :: LATTICE8:13

    

     Th13: for A be non empty set holds for L be lower-bounded LATTICE holds 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_fun2 (d,q))

    proof

      let A be non empty set;

      let L be lower-bounded LATTICE;

      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_fun2 (d,q));

      

       A1: A c= ( new_set2 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 Def4

        .= (g . [x, y]);

        hence thesis by A4;

      end;

      ( dom d) = [:A, A:] & ( dom g) = [:( new_set2 A), ( new_set2 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;

    reserve x for set,

C for Ordinal,

L0 for Sequence;

    definition

      let A be non empty set;

      let O be Ordinal;

      :: LATTICE8:def5

      func ConsecutiveSet2 (A,O) -> set means

      : Def5: 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_set2 (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( set, Sequence) = ( union ( rng $2));

        deffunc C( Ordinal, set) = ( new_set2 $2);

        (ex x be object, L0 st x = ( last L0) & ( dom L0) = ( succ O) & (L0 . 0 ) = A & (for C st ( succ C) in ( succ O) holds (L0 . ( succ C)) = C(C,.)) & for C st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L0 . C) = D(C,|)) & for x1,x2 be set st (ex L0 st x1 = ( last L0) & ( dom L0) = ( succ O) & (L0 . 0 ) = A & (for C st ( succ C) in ( succ O) holds (L0 . ( succ C)) = C(C,.)) & for C st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L0 . C) = D(C,|)) & (ex L0 st x2 = ( last L0) & ( dom L0) = ( succ O) & (L0 . 0 ) = A & (for C st ( succ C) in ( succ O) holds (L0 . ( succ C)) = C(C,.)) & for C st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L0 . C) = D(C,|)) holds x1 = x2 from ORDINAL2:sch 7;

        hence thesis;

      end;

    end

    theorem :: LATTICE8:14

    

     Th14: for A be non empty set holds ( ConsecutiveSet2 (A, 0 )) = A

    proof

      deffunc D( set, Sequence) = ( union ( rng $2));

      deffunc C( Ordinal, set) = ( new_set2 $2);

      let A be non empty set;

      deffunc F( Ordinal) = ( ConsecutiveSet2 (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)) = C(C,.)) & for C be Ordinal st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L0 . C) = D(C,|) by Def5;

      thus F(0) = A from ORDINAL2:sch 8( A1);

    end;

    theorem :: LATTICE8:15

    

     Th15: for A be non empty set holds for O be Ordinal holds ( ConsecutiveSet2 (A,( succ O))) = ( new_set2 ( ConsecutiveSet2 (A,O)))

    proof

      deffunc D( set, Sequence) = ( union ( rng $2));

      deffunc C( Ordinal, set) = ( new_set2 $2);

      let A be non empty set;

      let O be Ordinal;

      deffunc F( Ordinal) = ( ConsecutiveSet2 (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)) = C(C,.)) & for C be Ordinal st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L0 . C) = D(C,|) by Def5;

      for O be Ordinal holds F(succ) = C(O,F) from ORDINAL2:sch 9( A1);

      hence thesis;

    end;

    theorem :: LATTICE8:16

    

     Th16: for A be non empty set holds for O be Ordinal holds for T be Sequence holds O <> 0 & O is limit_ordinal & ( dom T) = O & (for O1 be Ordinal st O1 in O holds (T . O1) = ( ConsecutiveSet2 (A,O1))) implies ( ConsecutiveSet2 (A,O)) = ( union ( rng T))

    proof

      deffunc D( set, Sequence) = ( union ( rng $2));

      deffunc C( Ordinal, set) = ( new_set2 $2);

      let A be non empty set;

      let O be Ordinal;

      let T be Sequence;

      deffunc F( Ordinal) = ( ConsecutiveSet2 (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, 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)) = C(C,.)) & for C be Ordinal st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L0 . C) = D(C,|) by Def5;

      thus F(O) = D(O,T) from ORDINAL2:sch 10( A4, A1, A2, A3);

    end;

    reserve O1,O2 for Ordinal;

    registration

      let A be non empty set;

      let O be Ordinal;

      cluster ( ConsecutiveSet2 (A,O)) -> non empty;

      coherence

      proof

        defpred X[ Ordinal] means ( ConsecutiveSet2 (A,$1)) is non empty;

        

         A1: for O1 be Ordinal st X[O1] holds X[( succ O1)]

        proof

          let O1 be Ordinal;

          assume ( ConsecutiveSet2 (A,O1)) is non empty;

          ( ConsecutiveSet2 (A,( succ O1))) = ( new_set2 ( ConsecutiveSet2 (A,O1))) by Th15;

          hence thesis;

        end;

        

         A2: for O1 st O1 <> 0 & O1 is limit_ordinal & for O2 st O2 in O1 holds X[O2] holds X[O1]

        proof

          deffunc U( Ordinal) = ( ConsecutiveSet2 (A,$1));

          let O1 be Ordinal;

          assume that

           A3: O1 <> 0 and

           A4: O1 is limit_ordinal and for O2 be Ordinal st O2 in O1 holds ( ConsecutiveSet2 (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 . {} ) = ( ConsecutiveSet2 (A, {} )) by A3, A6, ORDINAL3: 8

          .= A by Th14;

          then

           A7: A in ( rng Ls) by A6, A5, FUNCT_1:def 3;

          ( ConsecutiveSet2 (A,O1)) = ( union ( rng Ls)) by A3, A4, A6, Th16;

          then A c= ( ConsecutiveSet2 (A,O1)) by A7, ZFMISC_1: 74;

          hence thesis;

        end;

        

         A8: X[ 0 ] by Th14;

        for O be Ordinal holds X[O] from ORDINAL2:sch 1( A8, A1, A2);

        hence thesis;

      end;

    end

    theorem :: LATTICE8:17

    

     Th17: for A be non empty set holds for O be Ordinal holds A c= ( ConsecutiveSet2 (A,O))

    proof

      let A be non empty set;

      let O be Ordinal;

      defpred X[ Ordinal] means A c= ( ConsecutiveSet2 (A,$1));

      

       A1: for O1 be Ordinal st X[O1] holds X[( succ O1)]

      proof

        let O1 be Ordinal;

        ( ConsecutiveSet2 (A,( succ O1))) = ( new_set2 ( ConsecutiveSet2 (A,O1))) by Th15;

        then

         A2: ( ConsecutiveSet2 (A,O1)) c= ( ConsecutiveSet2 (A,( succ O1))) by XBOOLE_1: 7;

        assume A c= ( ConsecutiveSet2 (A,O1));

        hence thesis by A2, XBOOLE_1: 1;

      end;

      

       A3: for O1 st O1 <> 0 & O1 is limit_ordinal & for O2 st O2 in O1 holds X[O2] holds X[O1]

      proof

        deffunc U( Ordinal) = ( ConsecutiveSet2 (A,$1));

        let O2 be Ordinal;

        assume that

         A4: O2 <> 0 and

         A5: O2 is limit_ordinal and for O1 be Ordinal st O1 in O2 holds A c= ( ConsecutiveSet2 (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 . {} ) = ( ConsecutiveSet2 (A, {} )) by A4, A7, ORDINAL3: 8

        .= A by Th14;

        then

         A8: A in ( rng Ls) by A7, A6, FUNCT_1:def 3;

        ( ConsecutiveSet2 (A,O2)) = ( union ( rng Ls)) by A4, A5, A7, Th16;

        hence thesis by A8, ZFMISC_1: 74;

      end;

      

       A9: X[ 0 ] by Th14;

      for O be Ordinal holds X[O] from ORDINAL2:sch 1( A9, A1, A3);

      hence thesis;

    end;

    definition

      let A be non empty set;

      let L be lower-bounded LATTICE;

      let d be BiFunction of A, L;

      let q be QuadrSeq of d;

      let O be Ordinal;

      assume

       A1: O in ( dom q);

      :: LATTICE8:def6

      func Quadr2 (q,O) -> Element of [:( ConsecutiveSet2 (A,O)), ( ConsecutiveSet2 (A,O)), the carrier of L, the carrier of L:] equals

      : Def6: (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 LATTICE5:def 13;

        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= ( ConsecutiveSet2 (A,O)) by Th17;

        then

        reconsider x, y as Element of ( ConsecutiveSet2 (A,O));

        reconsider z = [x, y, a, b] as Element of [:( ConsecutiveSet2 (A,O)), ( ConsecutiveSet2 (A,O)), the carrier of L, the carrier of L:];

        z = (q . O) by A2;

        hence thesis;

      end;

    end

    definition

      let A be non empty set;

      let L be lower-bounded LATTICE;

      let d be BiFunction of A, L;

      let q be QuadrSeq of d;

      let O be Ordinal;

      :: LATTICE8:def7

      func ConsecutiveDelta2 (q,O) -> set means

      : Def7: 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_fun2 (( BiFun ((L0 . C),( ConsecutiveSet2 (A,C)),L)),( Quadr2 (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( set, Sequence) = ( union ( rng $2));

        deffunc C( Ordinal, set) = ( new_bi_fun2 (( BiFun ($2,( ConsecutiveSet2 (A,$1)),L)),( Quadr2 (q,$1))));

        (ex x be object, L0 st x = ( last L0) & ( dom L0) = ( succ O) & (L0 . 0 ) = d & (for C st ( succ C) in ( succ O) holds (L0 . ( succ C)) = C(C,.)) & for C st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L0 . C) = D(C,|)) & for x1,x2 be set st (ex L0 st x1 = ( last L0) & ( dom L0) = ( succ O) & (L0 . 0 ) = d & (for C st ( succ C) in ( succ O) holds (L0 . ( succ C)) = C(C,.)) & for C st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L0 . C) = D(C,|)) & (ex L0 st x2 = ( last L0) & ( dom L0) = ( succ O) & (L0 . 0 ) = d & (for C st ( succ C) in ( succ O) holds (L0 . ( succ C)) = C(C,.)) & for C st C in ( succ O) & C <> 0 & C is limit_ordinal holds (L0 . C) = D(C,|)) holds x1 = x2 from ORDINAL2:sch 7;

        hence thesis;

      end;

    end

    theorem :: LATTICE8:18

    

     Th18: for A be non empty set holds for L be lower-bounded LATTICE holds for d be BiFunction of A, L holds for q be QuadrSeq of d holds ( ConsecutiveDelta2 (q, 0 )) = d

    proof

      deffunc D( set, Sequence) = ( union ( rng $2));

      let A be non empty set;

      let L be lower-bounded LATTICE;

      let d be BiFunction of A, L;

      let q be QuadrSeq of d;

      deffunc C( Ordinal, set) = ( new_bi_fun2 (( BiFun ($2,( ConsecutiveSet2 (A,$1)),L)),( Quadr2 (q,$1))));

      deffunc F( Ordinal) = ( ConsecutiveDelta2 (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 Def7;

      thus F(0) = d from ORDINAL2:sch 8( A1);

    end;

    theorem :: LATTICE8:19

    

     Th19: for A be non empty set holds for L be lower-bounded LATTICE holds for d be BiFunction of A, L holds for q be QuadrSeq of d holds for O be Ordinal holds ( ConsecutiveDelta2 (q,( succ O))) = ( new_bi_fun2 (( BiFun (( ConsecutiveDelta2 (q,O)),( ConsecutiveSet2 (A,O)),L)),( Quadr2 (q,O))))

    proof

      deffunc D( set, Sequence) = ( union ( rng $2));

      let A be non empty set;

      let L be lower-bounded LATTICE;

      let d be BiFunction of A, L;

      let q be QuadrSeq of d;

      let O be Ordinal;

      deffunc C( Ordinal, set) = ( new_bi_fun2 (( BiFun ($2,( ConsecutiveSet2 (A,$1)),L)),( Quadr2 (q,$1))));

      deffunc F( Ordinal) = ( ConsecutiveDelta2 (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 Def7;

      for O be Ordinal holds F(succ) = C(O,F) from ORDINAL2:sch 9( A1);

      hence thesis;

    end;

    theorem :: LATTICE8:20

    

     Th20: for A be non empty set holds for L be lower-bounded LATTICE holds for d be BiFunction of A, L holds for q be QuadrSeq of d holds for T be Sequence holds for O be Ordinal holds O <> 0 & O is limit_ordinal & ( dom T) = O & (for O1 be Ordinal st O1 in O holds (T . O1) = ( ConsecutiveDelta2 (q,O1))) implies ( ConsecutiveDelta2 (q,O)) = ( union ( rng T))

    proof

      deffunc D( set, Sequence) = ( union ( rng $2));

      let A be non empty set;

      let L be lower-bounded LATTICE;

      let d be BiFunction of A, L;

      let q be QuadrSeq of d;

      let T be Sequence;

      let O be Ordinal;

      deffunc C( Ordinal, set) = ( new_bi_fun2 (( BiFun ($2,( ConsecutiveSet2 (A,$1)),L)),( Quadr2 (q,$1))));

      deffunc F( Ordinal) = ( ConsecutiveDelta2 (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 Def7;

      thus F(O) = D(O,T) from ORDINAL2:sch 10( A4, A1, A2, A3);

    end;

    theorem :: LATTICE8:21

    

     Th21: for A be non empty set holds for O,O1,O2 be Ordinal holds O1 c= O2 implies ( ConsecutiveSet2 (A,O1)) c= ( ConsecutiveSet2 (A,O2))

    proof

      let A be non empty set;

      let O,O1,02 be Ordinal;

      defpred X[ Ordinal] means O1 c= $1 implies ( ConsecutiveSet2 (A,O1)) c= ( ConsecutiveSet2 (A,$1));

      

       A1: for O1 be Ordinal st X[O1] holds X[( succ O1)]

      proof

        let O2 be Ordinal;

        assume

         A2: O1 c= O2 implies ( ConsecutiveSet2 (A,O1)) c= ( ConsecutiveSet2 (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;

          ( ConsecutiveSet2 (A,O2)) c= ( new_set2 ( ConsecutiveSet2 (A,O2))) by XBOOLE_1: 7;

          then ( ConsecutiveSet2 (A,O1)) c= ( new_set2 ( ConsecutiveSet2 (A,O2))) by A2, A4, ORDINAL1: 22;

          hence thesis by Th15;

        end;

      end;

      

       A5: for O1 st O1 <> 0 & O1 is limit_ordinal & for O2 st O2 in O1 holds X[O2] holds X[O1]

      proof

        deffunc U( Ordinal) = ( ConsecutiveSet2 (A,$1));

        let O2 be Ordinal;

        assume that

         A6: O2 <> 0 & O2 is limit_ordinal and for O3 be Ordinal st O3 in O2 holds O1 c= O3 implies ( ConsecutiveSet2 (A,O1)) c= ( ConsecutiveSet2 (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: ( ConsecutiveSet2 (A,O2)) = ( union ( rng L)) by A6, A7, Th16;

        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) = ( ConsecutiveSet2 (A,O1)) by A7, A10, ORDINAL1: 11;

          hence thesis by A8, A11, ZFMISC_1: 74;

        end;

      end;

      

       A12: X[ 0 ];

      for O be Ordinal holds X[O] from ORDINAL2:sch 1( A12, A1, A5);

      hence thesis;

    end;

    theorem :: LATTICE8:22

    

     Th22: for A be non empty set holds for L be lower-bounded LATTICE holds for d be BiFunction of A, L holds for q be QuadrSeq of d holds for O be Ordinal holds ( ConsecutiveDelta2 (q,O)) is BiFunction of ( ConsecutiveSet2 (A,O)), L

    proof

      let A be non empty set;

      let L be lower-bounded LATTICE;

      let d be BiFunction of A, L;

      let q be QuadrSeq of d;

      let O be Ordinal;

      defpred X[ Ordinal] means ( ConsecutiveDelta2 (q,$1)) is BiFunction of ( ConsecutiveSet2 (A,$1)), L;

      

       A1: for O1 be Ordinal st X[O1] holds X[( succ O1)]

      proof

        let O1 be Ordinal;

        assume ( ConsecutiveDelta2 (q,O1)) is BiFunction of ( ConsecutiveSet2 (A,O1)), L;

        then

        reconsider CD = ( ConsecutiveDelta2 (q,O1)) as BiFunction of ( ConsecutiveSet2 (A,O1)), L;

        

         A2: ( ConsecutiveDelta2 (q,( succ O1))) = ( new_bi_fun2 (( BiFun (( ConsecutiveDelta2 (q,O1)),( ConsecutiveSet2 (A,O1)),L)),( Quadr2 (q,O1)))) by Th19

        .= ( new_bi_fun2 (CD,( Quadr2 (q,O1)))) by LATTICE5:def 15;

        ( ConsecutiveSet2 (A,( succ O1))) = ( new_set2 ( ConsecutiveSet2 (A,O1))) by Th15;

        hence thesis by A2;

      end;

      

       A3: for O1 st O1 <> 0 & O1 is limit_ordinal & for O2 st O2 in O1 holds X[O2] holds X[O1]

      proof

        deffunc U( Ordinal) = ( ConsecutiveDelta2 (q,$1));

        let O1 be Ordinal;

        assume that

         A4: O1 <> 0 and

         A5: O1 is limit_ordinal and

         A6: for O2 be Ordinal st O2 in O1 holds ( ConsecutiveDelta2 (q,O2)) is BiFunction of ( ConsecutiveSet2 (A,O2)), L;

        reconsider o1 = O1 as non empty Ordinal by A4;

        set YY = the set of all [:( ConsecutiveSet2 (A,O2)), ( ConsecutiveSet2 (A,O2)):] where O2 be Element of o1;

        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 be Ordinal st O c= O2 & O2 in ( dom Ls) holds (Ls . O) c= (Ls . O2)

        proof

          let O be Ordinal;

          defpred X[ Ordinal] means O c= $1 & $1 in ( dom Ls) implies (Ls . O) c= (Ls . $1);

          

           A9: for O1 st O1 <> 0 & O1 is limit_ordinal & for O2 st O2 in O1 holds X[O2] holds X[O1]

          proof

            deffunc U( Ordinal) = ( ConsecutiveDelta2 (q,$1));

            let O2 be Ordinal;

            assume that

             A10: O2 <> 0 & O2 is limit_ordinal and for O3 be Ordinal 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) = ( ConsecutiveDelta2 (q,O2)) by A7, A12

            .= ( union ( rng Lt)) by A10, A13, Th20;

            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) = ( ConsecutiveDelta2 (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 O1 be Ordinal st X[O1] holds X[( succ O1)]

          proof

            let O2 be Ordinal;

            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 Def8 = ( ConsecutiveDelta2 (q,O2)) as BiFunction of ( ConsecutiveSet2 (A,O2)), L by A6, A7;

              (Ls . ( succ O2)) = ( ConsecutiveDelta2 (q,( succ O2))) by A7, A20

              .= ( new_bi_fun2 (( BiFun (( ConsecutiveDelta2 (q,O2)),( ConsecutiveSet2 (A,O2)),L)),( Quadr2 (q,O2)))) by Th19

              .= ( new_bi_fun2 (Def8,( Quadr2 (q,O2)))) by LATTICE5:def 15;

              then ( ConsecutiveDelta2 (q,O2)) c= (Ls . ( succ O2)) by Th13;

              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 O be Ordinal holds X[O] 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 = [:( ConsecutiveSet2 (A,O1)), ( ConsecutiveSet2 (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) = ( ConsecutiveDelta2 (q,o)) by A7, A31;

          then

          reconsider h = (Ls . o) as BiFunction of ( ConsecutiveSet2 (A,o)), L by A6, A7, A31;

          o c= O1 by A7, A31, ORDINAL1:def 2;

          then ( dom h) = [:( ConsecutiveSet2 (A,o)), ( ConsecutiveSet2 (A,o)):] & ( ConsecutiveSet2 (A,o)) c= ( ConsecutiveSet2 (A,O1)) by Th21, 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;

        Ls is Function-yielding

        proof

          let x be object;

          assume

           A34: x in ( dom Ls);

          then

          reconsider o = x as Ordinal;

          (Ls . o) = ( ConsecutiveDelta2 (q,o)) by A7, A34;

          hence thesis by A6, A7, A34;

        end;

        then

        reconsider LsF = Ls as Function-yielding Function;

        

         A35: ( 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

             A36: o in ( dom ( doms LsF)) and

             A37: Z = (( doms LsF) . o) by FUNCT_1:def 3;

            

             A38: o in ( dom LsF) by A36, FUNCT_6: 59;

            then

            reconsider o9 = o as Element of o1 by A7;

            (Ls . o9) = ( ConsecutiveDelta2 (q,o9)) by A7;

            then

            reconsider ls = (Ls . o9) as BiFunction of ( ConsecutiveSet2 (A,o9)), L by A6;

            Z = ( dom ls) by A37, A38, FUNCT_6: 22

            .= [:( ConsecutiveSet2 (A,o9)), ( ConsecutiveSet2 (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

           A39: Z = [:( ConsecutiveSet2 (A,o)), ( ConsecutiveSet2 (A,o)):];

          (Ls . o) = ( ConsecutiveDelta2 (q,o)) by A7;

          then

          reconsider ls = (Ls . o) as BiFunction of ( ConsecutiveSet2 (A,o)), L by A6;

          o in ( dom LsF) by A7;

          then

           A40: o in ( dom ( doms LsF)) by FUNCT_6: 59;

          Z = ( dom ls) by A39, FUNCT_2:def 1

          .= (( doms LsF) . o) by A7, FUNCT_6: 22;

          hence thesis by A40, FUNCT_1:def 3;

        end;

        

         A41: ( ConsecutiveDelta2 (q,O1)) = ( union ( rng Ls)) by A4, A5, A7, Th20;

        reconsider f as Function by A33;

        deffunc U( Ordinal) = ( ConsecutiveSet2 (A,$1));

        consider Ts be Sequence such that

         A42: ( dom Ts) = O1 & for O2 be Ordinal st O2 in O1 holds (Ts . O2) = U(O2) from ORDINAL2:sch 2;

         {} in O1 by A4, ORDINAL3: 8;

        then

        reconsider RTs = ( rng Ts) as non empty set by A42, FUNCT_1: 3;

        

         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 = [:( ConsecutiveSet2 (A,o)), ( ConsecutiveSet2 (A,o)):];

            (Ts . o) = ( ConsecutiveSet2 (A,o)) by A42;

            then

            reconsider CoS = ( ConsecutiveSet2 (A,o)) as Element of RTs by A42, 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 = ( ConsecutiveSet2 (A,o9)) by A42, A46, A47;

          hence thesis by A42, 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) = ( ConsecutiveSet2 (A,o29)) by A42, A52;

          

           A55: o19 c= o29 or o29 c= o19;

          (Ts . o19) = ( ConsecutiveSet2 (A,o19)) by A42, A50;

          then x c= y or y c= x by A51, A53, A54, A55, Th21;

          hence thesis;

        end;

        then

         A56: ( dom f) = ( union ( rng ( doms LsF))) & RTs is c=-linear by LATTICE5: 1;

        X = [:( union ( rng Ts)), ( ConsecutiveSet2 (A,O1)):] by A4, A5, A42, Th16

        .= [:( union RTs), ( union RTs):] by A4, A5, A42, Th16

        .= ( dom f) by A35, A56, A43, LATTICE5: 3;

        hence thesis by A41, A33, FUNCT_2:def 1, RELSET_1: 4;

      end;

      ( ConsecutiveSet2 (A, {} )) = A by Th14;

      then

       A57: X[ 0 ] by Th18;

      for O be Ordinal holds X[O] from ORDINAL2:sch 1( A57, A1, A3);

      hence thesis;

    end;

    definition

      let A be non empty set;

      let L be lower-bounded LATTICE;

      let d be BiFunction of A, L;

      let q be QuadrSeq of d;

      let O be Ordinal;

      :: original: ConsecutiveDelta2

      redefine

      func ConsecutiveDelta2 (q,O) -> BiFunction of ( ConsecutiveSet2 (A,O)), L ;

      coherence by Th22;

    end

    theorem :: LATTICE8:23

    

     Th23: for A be non empty set holds for L be lower-bounded LATTICE holds for d be BiFunction of A, L holds for q be QuadrSeq of d holds for O be Ordinal holds d c= ( ConsecutiveDelta2 (q,O))

    proof

      let A be non empty set;

      let L be lower-bounded LATTICE;

      let d be BiFunction of A, L;

      let q be QuadrSeq of d;

      let O be Ordinal;

      defpred X[ Ordinal] means d c= ( ConsecutiveDelta2 (q,$1));

      

       A1: for O1 be Ordinal st X[O1] holds X[( succ O1)]

      proof

        let O1 be Ordinal;

        ( ConsecutiveDelta2 (q,( succ O1))) = ( new_bi_fun2 (( BiFun (( ConsecutiveDelta2 (q,O1)),( ConsecutiveSet2 (A,O1)),L)),( Quadr2 (q,O1)))) by Th19

        .= ( new_bi_fun2 (( ConsecutiveDelta2 (q,O1)),( Quadr2 (q,O1)))) by LATTICE5:def 15;

        then

         A2: ( ConsecutiveDelta2 (q,O1)) c= ( ConsecutiveDelta2 (q,( succ O1))) by Th13;

        assume d c= ( ConsecutiveDelta2 (q,O1));

        hence thesis by A2, XBOOLE_1: 1;

      end;

      

       A3: for O1 st O1 <> 0 & O1 is limit_ordinal & for O2 st O2 in O1 holds X[O2] holds X[O1]

      proof

        deffunc U( Ordinal) = ( ConsecutiveDelta2 (q,$1));

        let O2 be Ordinal;

        assume that

         A4: O2 <> 0 and

         A5: O2 is limit_ordinal and for O1 be Ordinal st O1 in O2 holds d c= ( ConsecutiveDelta2 (q,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 . {} ) = ( ConsecutiveDelta2 (q, {} )) by A4, A7, ORDINAL3: 8

        .= d by Th18;

        then

         A8: d in ( rng Ls) by A7, A6, FUNCT_1:def 3;

        ( ConsecutiveDelta2 (q,O2)) = ( union ( rng Ls)) by A4, A5, A7, Th20;

        hence thesis by A8, ZFMISC_1: 74;

      end;

      

       A9: X[ 0 ] by Th18;

      for O be Ordinal holds X[O] from ORDINAL2:sch 1( A9, A1, A3);

      hence thesis;

    end;

    theorem :: LATTICE8:24

    

     Th24: for A be non empty set holds for L be lower-bounded LATTICE holds for d be BiFunction of A, L holds for O1,O2 be Ordinal holds for q be QuadrSeq of d st O1 c= O2 holds ( ConsecutiveDelta2 (q,O1)) c= ( ConsecutiveDelta2 (q,O2))

    proof

      let A be non empty set;

      let L be lower-bounded LATTICE;

      let d be BiFunction of A, L;

      let O1,O2 be Ordinal;

      let q be QuadrSeq of d;

      defpred X[ Ordinal] means O1 c= $1 implies ( ConsecutiveDelta2 (q,O1)) c= ( ConsecutiveDelta2 (q,$1));

      

       A1: for O1 st O1 <> 0 & O1 is limit_ordinal & for O2 st O2 in O1 holds X[O2] holds X[O1]

      proof

        deffunc U( Ordinal) = ( ConsecutiveDelta2 (q,$1));

        let O2 be Ordinal;

        assume that

         A2: O2 <> 0 & O2 is limit_ordinal and for O3 be Ordinal st O3 in O2 holds O1 c= O3 implies ( ConsecutiveDelta2 (q,O1)) c= ( ConsecutiveDelta2 (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: ( ConsecutiveDelta2 (q,O2)) = ( union ( rng L)) by A2, A3, Th20;

        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) = ( ConsecutiveDelta2 (q,O1)) by A3, A6, ORDINAL1: 11;

          hence thesis by A4, A7, ZFMISC_1: 74;

        end;

      end;

      

       A8: for O1 be Ordinal st X[O1] holds X[( succ O1)]

      proof

        let O2 be Ordinal;

        assume

         A9: O1 c= O2 implies ( ConsecutiveDelta2 (q,O1)) c= ( ConsecutiveDelta2 (q,O2));

        assume

         A10: O1 c= ( succ O2);

        per cases ;

          suppose O1 = ( succ O2);

          hence thesis;

        end;

          suppose

           A11: O1 <> ( succ O2);

          ( ConsecutiveDelta2 (q,( succ O2))) = ( new_bi_fun2 (( BiFun (( ConsecutiveDelta2 (q,O2)),( ConsecutiveSet2 (A,O2)),L)),( Quadr2 (q,O2)))) by Th19

          .= ( new_bi_fun2 (( ConsecutiveDelta2 (q,O2)),( Quadr2 (q,O2)))) by LATTICE5:def 15;

          then

           A12: ( ConsecutiveDelta2 (q,O2)) c= ( ConsecutiveDelta2 (q,( succ O2))) by Th13;

          O1 c< ( succ O2) by A10, A11;

          then O1 in ( succ O2) by ORDINAL1: 11;

          hence thesis by A9, A12, ORDINAL1: 22;

        end;

      end;

      

       A13: X[ 0 ];

      for O be Ordinal holds X[O] from ORDINAL2:sch 1( A13, A8, A1);

      hence thesis;

    end;

    theorem :: LATTICE8:25

    

     Th25: for A be non empty set holds for L be lower-bounded LATTICE holds for d be BiFunction of A, L st d is zeroed holds for q be QuadrSeq of d holds for O be Ordinal holds ( ConsecutiveDelta2 (q,O)) is zeroed

    proof

      let A be non empty set;

      let L be lower-bounded LATTICE;

      let d be BiFunction of A, L;

      assume

       A1: d is zeroed;

      let q be QuadrSeq of d;

      let O be Ordinal;

      defpred X[ Ordinal] means ( ConsecutiveDelta2 (q,$1)) is zeroed;

      

       A2: for O1 be Ordinal st X[O1] holds X[( succ O1)]

      proof

        let O1 be Ordinal;

        assume ( ConsecutiveDelta2 (q,O1)) is zeroed;

        then

         A3: ( new_bi_fun2 (( ConsecutiveDelta2 (q,O1)),( Quadr2 (q,O1)))) is zeroed by Th10;

        let z be Element of ( ConsecutiveSet2 (A,( succ O1)));

        reconsider z9 = z as Element of ( new_set2 ( ConsecutiveSet2 (A,O1))) by Th15;

        ( ConsecutiveDelta2 (q,( succ O1))) = ( new_bi_fun2 (( BiFun (( ConsecutiveDelta2 (q,O1)),( ConsecutiveSet2 (A,O1)),L)),( Quadr2 (q,O1)))) by Th19

        .= ( new_bi_fun2 (( ConsecutiveDelta2 (q,O1)),( Quadr2 (q,O1)))) by LATTICE5:def 15;

        

        hence (( ConsecutiveDelta2 (q,( succ O1))) . (z,z)) = (( new_bi_fun2 (( ConsecutiveDelta2 (q,O1)),( Quadr2 (q,O1)))) . (z9,z9))

        .= ( Bottom L) by A3;

      end;

      

       A4: for O1 st O1 <> 0 & O1 is limit_ordinal & for O2 st O2 in O1 holds X[O2] holds X[O1]

      proof

        deffunc U( Ordinal) = ( ConsecutiveDelta2 (q,$1));

        let O2 be Ordinal;

        assume that

         A5: O2 <> 0 & O2 is limit_ordinal and

         A6: for O1 be Ordinal st O1 in O2 holds ( ConsecutiveDelta2 (q,O1)) is zeroed;

        set CS = ( ConsecutiveSet2 (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;

        ( ConsecutiveDelta2 (q,O2)) = ( union ( rng Ls)) by A5, A7, Th20;

        then

        reconsider f = ( union ( rng Ls)) as BiFunction of CS, L;

        deffunc U( Ordinal) = ( ConsecutiveSet2 (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: ( ConsecutiveSet2 (A,O2)) = ( union ( rng Ts)) by A5, A8, Th16;

        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) = ( ConsecutiveDelta2 (q,o)) by A7, A8, A12;

          then

          reconsider h = (Ls . o) as BiFunction of ( ConsecutiveSet2 (A,o)), L;

          reconsider x9 = x as Element of ( ConsecutiveSet2 (A,o)) by A8, A10, A12, A13;

          

           A15: ( dom h) = [:( ConsecutiveSet2 (A,o)), ( ConsecutiveSet2 (A,o)):] by FUNCT_2:def 1;

          

           A16: h is zeroed

          proof

            let z be Element of ( ConsecutiveSet2 (A,o));

            

             A17: ( ConsecutiveDelta2 (q,o)) is zeroed by A6, A8, A12;

            

            thus (h . (z,z)) = (( ConsecutiveDelta2 (q,o)) . (z,z)) by A7, A8, A12

            .= ( Bottom L) by A17;

          end;

          ( ConsecutiveDelta2 (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 ( ConsecutiveSet2 (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, Th20;

      end;

      

       A19: X[ 0 ]

      proof

        let z be Element of ( ConsecutiveSet2 (A, 0 ));

        reconsider z9 = z as Element of A by Th14;

        

        thus (( ConsecutiveDelta2 (q, 0 )) . (z,z)) = (d . (z9,z9)) by Th18

        .= ( Bottom L) by A1;

      end;

      for O be Ordinal holds X[O] from ORDINAL2:sch 1( A19, A2, A4);

      hence thesis;

    end;

    theorem :: LATTICE8:26

    

     Th26: for A be non empty set holds for L be lower-bounded LATTICE holds for d be BiFunction of A, L st d is symmetric holds for q be QuadrSeq of d holds for O be Ordinal holds ( ConsecutiveDelta2 (q,O)) is symmetric

    proof

      let A be non empty set;

      let L be lower-bounded LATTICE;

      let d be BiFunction of A, L;

      assume

       A1: d is symmetric;

      let q be QuadrSeq of d;

      let O be Ordinal;

      defpred X[ Ordinal] means ( ConsecutiveDelta2 (q,$1)) is symmetric;

      

       A2: for O1 be Ordinal st X[O1] holds X[( succ O1)]

      proof

        let O1 be Ordinal;

        assume ( ConsecutiveDelta2 (q,O1)) is symmetric;

        then

         A3: ( new_bi_fun2 (( ConsecutiveDelta2 (q,O1)),( Quadr2 (q,O1)))) is symmetric by Th11;

        let x,y be Element of ( ConsecutiveSet2 (A,( succ O1)));

        reconsider x9 = x, y9 = y as Element of ( new_set2 ( ConsecutiveSet2 (A,O1))) by Th15;

        

         A4: ( ConsecutiveDelta2 (q,( succ O1))) = ( new_bi_fun2 (( BiFun (( ConsecutiveDelta2 (q,O1)),( ConsecutiveSet2 (A,O1)),L)),( Quadr2 (q,O1)))) by Th19

        .= ( new_bi_fun2 (( ConsecutiveDelta2 (q,O1)),( Quadr2 (q,O1)))) by LATTICE5:def 15;

        

        hence (( ConsecutiveDelta2 (q,( succ O1))) . (x,y)) = (( new_bi_fun2 (( ConsecutiveDelta2 (q,O1)),( Quadr2 (q,O1)))) . (y9,x9)) by A3

        .= (( ConsecutiveDelta2 (q,( succ O1))) . (y,x)) by A4;

      end;

      

       A5: for O1 st O1 <> 0 & O1 is limit_ordinal & for O2 st O2 in O1 holds X[O2] holds X[O1]

      proof

        deffunc U( Ordinal) = ( ConsecutiveDelta2 (q,$1));

        let O2 be Ordinal;

        assume that

         A6: O2 <> 0 & O2 is limit_ordinal and

         A7: for O1 be Ordinal st O1 in O2 holds ( ConsecutiveDelta2 (q,O1)) is symmetric;

        set CS = ( ConsecutiveSet2 (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;

        ( ConsecutiveDelta2 (q,O2)) = ( union ( rng Ls)) by A6, A8, Th20;

        then

        reconsider f = ( union ( rng Ls)) as BiFunction of CS, L;

        deffunc U( Ordinal) = ( ConsecutiveSet2 (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: ( ConsecutiveSet2 (A,O2)) = ( union ( rng Ts)) by A6, A9, Th16;

        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 ( ConsecutiveSet2 (A,o1)) by A9, A11, A13, A14;

          

           A20: (Ls . o1) = ( ConsecutiveDelta2 (q,o1)) by A8, A9, A13;

          then

          reconsider h1 = (Ls . o1) as BiFunction of ( ConsecutiveSet2 (A,o1)), L;

          

           A21: h1 is symmetric

          proof

            let x,y be Element of ( ConsecutiveSet2 (A,o1));

            

             A22: ( ConsecutiveDelta2 (q,o1)) is symmetric by A7, A9, A13;

            

            thus (h1 . (x,y)) = (( ConsecutiveDelta2 (q,o1)) . (x,y)) by A8, A9, A13

            .= (( ConsecutiveDelta2 (q,o1)) . (y,x)) by A22

            .= (h1 . (y,x)) by A8, A9, A13;

          end;

          

           A23: ( dom h1) = [:( ConsecutiveSet2 (A,o1)), ( ConsecutiveSet2 (A,o1)):] by FUNCT_2:def 1;

          

           A24: y in ( ConsecutiveSet2 (A,o2)) by A9, A15, A17, A18;

          

           A25: (Ls . o2) = ( ConsecutiveDelta2 (q,o2)) by A8, A9, A17;

          then

          reconsider h2 = (Ls . o2) as BiFunction of ( ConsecutiveSet2 (A,o2)), L;

          

           A26: h2 is symmetric

          proof

            let x,y be Element of ( ConsecutiveSet2 (A,o2));

            

             A27: ( ConsecutiveDelta2 (q,o2)) is symmetric by A7, A9, A17;

            

            thus (h2 . (x,y)) = (( ConsecutiveDelta2 (q,o2)) . (x,y)) by A8, A9, A17

            .= (( ConsecutiveDelta2 (q,o2)) . (y,x)) by A27

            .= (h2 . (y,x)) by A8, A9, A17;

          end;

          

           A28: ( dom h2) = [:( ConsecutiveSet2 (A,o2)), ( ConsecutiveSet2 (A,o2)):] by FUNCT_2:def 1;

          per cases ;

            suppose o1 c= o2;

            then

             A29: ( ConsecutiveSet2 (A,o1)) c= ( ConsecutiveSet2 (A,o2)) by Th21;

            then

             A30: [y, x] in ( dom h2) by A19, A24, A28, ZFMISC_1: 87;

            ( ConsecutiveDelta2 (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 ( ConsecutiveSet2 (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: ( ConsecutiveSet2 (A,o2)) c= ( ConsecutiveSet2 (A,o1)) by Th21;

            then

             A33: [y, x] in ( dom h1) by A19, A24, A23, ZFMISC_1: 87;

            ( ConsecutiveDelta2 (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 ( ConsecutiveSet2 (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, Th20;

      end;

      

       A35: X[ 0 ]

      proof

        let x,y be Element of ( ConsecutiveSet2 (A, 0 ));

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

        

        thus (( ConsecutiveDelta2 (q, 0 )) . (x,y)) = (d . (x9,y9)) by Th18

        .= (d . (y9,x9)) by A1

        .= (( ConsecutiveDelta2 (q, 0 )) . (y,x)) by Th18;

      end;

      for O be Ordinal holds X[O] from ORDINAL2:sch 1( A35, A2, A5);

      hence thesis;

    end;

    theorem :: LATTICE8:27

    

     Th27: for A be non empty set holds for L be lower-bounded LATTICE st L is modular holds for d be BiFunction of A, L st d is symmetric u.t.i. holds for O be Ordinal holds for q be QuadrSeq of d st O c= ( DistEsti d) holds ( ConsecutiveDelta2 (q,O)) is u.t.i.

    proof

      let A be non empty set;

      let L be lower-bounded LATTICE;

      assume

       A1: L is modular;

      let d be BiFunction of A, L;

      assume that

       A2: d is symmetric and

       A3: d is u.t.i.;

      let O be Ordinal;

      let q be QuadrSeq of d;

      defpred X[ Ordinal] means $1 c= ( DistEsti d) implies ( ConsecutiveDelta2 (q,$1)) is u.t.i.;

      

       A4: for O1 be Ordinal st X[O1] holds X[( succ O1)]

      proof

        let O1 be Ordinal;

        assume that

         A5: O1 c= ( DistEsti d) implies ( ConsecutiveDelta2 (q,O1)) is u.t.i. and

         A6: ( succ O1) c= ( DistEsti d);

        

         A7: O1 in ( DistEsti d) by A6, ORDINAL1: 21;

        then

         A8: O1 in ( dom q) by LATTICE5: 25;

        then (q . O1) in ( rng q) by FUNCT_1:def 3;

        then

         A9: (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 LATTICE5:def 13;

        let x,y,z be Element of ( ConsecutiveSet2 (A,( succ O1)));

        

         A10: ( ConsecutiveDelta2 (q,O1)) is symmetric by A2, Th26;

        reconsider x9 = x, y9 = y, z9 = z as Element of ( new_set2 ( ConsecutiveSet2 (A,O1))) by Th15;

        set f = ( new_bi_fun2 (( ConsecutiveDelta2 (q,O1)),( Quadr2 (q,O1))));

        set X = (( Quadr2 (q,O1)) `1_4 ), Y = (( Quadr2 (q,O1)) `2_4 );

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

        

         A11: ( dom d) = [:A, A:] & d c= ( ConsecutiveDelta2 (q,O1)) by Th23, FUNCT_2:def 1;

        consider u,v be Element of A, a9,b9 be Element of L such that

         A12: (q . O1) = [u, v, a9, b9] and

         A13: (d . (u,v)) <= (a9 "\/" b9) by A9;

        

         A14: ( Quadr2 (q,O1)) = [u, v, a9, b9] by A8, A12, Def6;

        then

         A15: u = X & v = Y;

        

         A16: a9 = a & b9 = b by A14;

        (d . (u,v)) = (d . [u, v])

        .= (( ConsecutiveDelta2 (q,O1)) . (X,Y)) by A15, A11, GRFUNC_1: 2;

        then ( new_bi_fun2 (( ConsecutiveDelta2 (q,O1)),( Quadr2 (q,O1)))) is u.t.i. by A1, A5, A7, A10, A13, A16, Th12, ORDINAL1:def 2;

        then

         A17: (f . (x9,z9)) <= ((f . (x9,y9)) "\/" (f . (y9,z9)));

        ( ConsecutiveDelta2 (q,( succ O1))) = ( new_bi_fun2 (( BiFun (( ConsecutiveDelta2 (q,O1)),( ConsecutiveSet2 (A,O1)),L)),( Quadr2 (q,O1)))) by Th19

        .= ( new_bi_fun2 (( ConsecutiveDelta2 (q,O1)),( Quadr2 (q,O1)))) by LATTICE5:def 15;

        hence (( ConsecutiveDelta2 (q,( succ O1))) . (x,z)) <= ((( ConsecutiveDelta2 (q,( succ O1))) . (x,y)) "\/" (( ConsecutiveDelta2 (q,( succ O1))) . (y,z))) by A17;

      end;

      

       A18: for O1 st O1 <> 0 & O1 is limit_ordinal & for O2 st O2 in O1 holds X[O2] holds X[O1]

      proof

        deffunc U( Ordinal) = ( ConsecutiveDelta2 (q,$1));

        let O2 be Ordinal;

        assume that

         A19: O2 <> 0 & O2 is limit_ordinal and

         A20: for O1 be Ordinal st O1 in O2 holds (O1 c= ( DistEsti d) implies ( ConsecutiveDelta2 (q,O1)) is u.t.i.) and

         A21: O2 c= ( DistEsti d);

        set CS = ( ConsecutiveSet2 (A,O2));

        consider Ls be Sequence such that

         A22: ( dom Ls) = O2 & for O1 be Ordinal st O1 in O2 holds (Ls . O1) = U(O1) from ORDINAL2:sch 2;

        ( ConsecutiveDelta2 (q,O2)) = ( union ( rng Ls)) by A19, A22, Th20;

        then

        reconsider f = ( union ( rng Ls)) as BiFunction of CS, L;

        deffunc U( Ordinal) = ( ConsecutiveSet2 (A,$1));

        consider Ts be Sequence such that

         A23: ( dom Ts) = O2 & for O1 be Ordinal st O1 in O2 holds (Ts . O1) = U(O1) from ORDINAL2:sch 2;

        

         A24: ( ConsecutiveSet2 (A,O2)) = ( union ( rng Ts)) by A19, A23, Th16;

        f is u.t.i.

        proof

          let x,y,z be Element of CS;

          consider X be set such that

           A25: x in X and

           A26: X in ( rng Ts) by A24, TARSKI:def 4;

          consider o1 be object such that

           A27: o1 in ( dom Ts) and

           A28: X = (Ts . o1) by A26, FUNCT_1:def 3;

          consider Y be set such that

           A29: y in Y and

           A30: Y in ( rng Ts) by A24, TARSKI:def 4;

          consider o2 be object such that

           A31: o2 in ( dom Ts) and

           A32: Y = (Ts . o2) by A30, FUNCT_1:def 3;

          consider Z be set such that

           A33: z in Z and

           A34: Z in ( rng Ts) by A24, TARSKI:def 4;

          consider o3 be object such that

           A35: o3 in ( dom Ts) and

           A36: Z = (Ts . o3) by A34, FUNCT_1:def 3;

          reconsider o1, o2, o3 as Ordinal by A27, A31, A35;

          

           A37: x in ( ConsecutiveSet2 (A,o1)) by A23, A25, A27, A28;

          

           A38: (Ls . o3) = ( ConsecutiveDelta2 (q,o3)) by A22, A23, A35;

          then

          reconsider h3 = (Ls . o3) as BiFunction of ( ConsecutiveSet2 (A,o3)), L;

          

           A39: h3 is u.t.i.

          proof

            let x,y,z be Element of ( ConsecutiveSet2 (A,o3));

            o3 c= ( DistEsti d) by A21, A23, A35, ORDINAL1:def 2;

            then

             A40: ( ConsecutiveDelta2 (q,o3)) is u.t.i. by A20, A23, A35;

            ( ConsecutiveDelta2 (q,o3)) = h3 by A22, A23, A35;

            hence (h3 . (x,z)) <= ((h3 . (x,y)) "\/" (h3 . (y,z))) by A40;

          end;

          

           A41: ( dom h3) = [:( ConsecutiveSet2 (A,o3)), ( ConsecutiveSet2 (A,o3)):] by FUNCT_2:def 1;

          

           A42: z in ( ConsecutiveSet2 (A,o3)) by A23, A33, A35, A36;

          

           A43: (Ls . o2) = ( ConsecutiveDelta2 (q,o2)) by A22, A23, A31;

          then

          reconsider h2 = (Ls . o2) as BiFunction of ( ConsecutiveSet2 (A,o2)), L;

          

           A44: h2 is u.t.i.

          proof

            let x,y,z be Element of ( ConsecutiveSet2 (A,o2));

            o2 c= ( DistEsti d) by A21, A23, A31, ORDINAL1:def 2;

            then

             A45: ( ConsecutiveDelta2 (q,o2)) is u.t.i. by A20, A23, A31;

            ( ConsecutiveDelta2 (q,o2)) = h2 by A22, A23, A31;

            hence (h2 . (x,z)) <= ((h2 . (x,y)) "\/" (h2 . (y,z))) by A45;

          end;

          

           A46: ( dom h2) = [:( ConsecutiveSet2 (A,o2)), ( ConsecutiveSet2 (A,o2)):] by FUNCT_2:def 1;

          

           A47: (Ls . o1) = ( ConsecutiveDelta2 (q,o1)) by A22, A23, A27;

          then

          reconsider h1 = (Ls . o1) as BiFunction of ( ConsecutiveSet2 (A,o1)), L;

          

           A48: h1 is u.t.i.

          proof

            let x,y,z be Element of ( ConsecutiveSet2 (A,o1));

            o1 c= ( DistEsti d) by A21, A23, A27, ORDINAL1:def 2;

            then

             A49: ( ConsecutiveDelta2 (q,o1)) is u.t.i. by A20, A23, A27;

            ( ConsecutiveDelta2 (q,o1)) = h1 by A22, A23, A27;

            hence (h1 . (x,z)) <= ((h1 . (x,y)) "\/" (h1 . (y,z))) by A49;

          end;

          

           A50: ( dom h1) = [:( ConsecutiveSet2 (A,o1)), ( ConsecutiveSet2 (A,o1)):] by FUNCT_2:def 1;

          

           A51: y in ( ConsecutiveSet2 (A,o2)) by A23, A29, A31, A32;

          per cases ;

            suppose

             A52: o1 c= o3;

            then

             A53: ( ConsecutiveSet2 (A,o1)) c= ( ConsecutiveSet2 (A,o3)) by Th21;

            thus ((f . (x,y)) "\/" (f . (y,z))) >= (f . (x,z))

            proof

              per cases ;

                suppose

                 A54: o2 c= o3;

                reconsider z9 = z as Element of ( ConsecutiveSet2 (A,o3)) by A23, A33, A35, A36;

                reconsider x9 = x as Element of ( ConsecutiveSet2 (A,o3)) by A37, A53;

                ( ConsecutiveDelta2 (q,o3)) in ( rng Ls) by A22, A23, A35, A38, FUNCT_1:def 3;

                then

                 A55: h3 c= f by A38, ZFMISC_1: 74;

                

                 A56: ( ConsecutiveSet2 (A,o2)) c= ( ConsecutiveSet2 (A,o3)) by A54, Th21;

                then

                reconsider y9 = y as Element of ( ConsecutiveSet2 (A,o3)) by A51;

                 [y, z] in ( dom h3) by A51, A42, A41, A56, ZFMISC_1: 87;

                then

                 A57: (f . (y,z)) = (h3 . (y9,z9)) by A55, GRFUNC_1: 2;

                 [x, z] in ( dom h3) by A37, A42, A41, A53, ZFMISC_1: 87;

                then

                 A58: (f . (x,z)) = (h3 . (x9,z9)) by A55, GRFUNC_1: 2;

                 [x, y] in ( dom h3) by A37, A51, A41, A53, A56, ZFMISC_1: 87;

                then (f . (x,y)) = (h3 . (x9,y9)) by A55, GRFUNC_1: 2;

                hence thesis by A39, A57, A58;

              end;

                suppose

                 A59: o3 c= o2;

                reconsider y9 = y as Element of ( ConsecutiveSet2 (A,o2)) by A23, A29, A31, A32;

                ( ConsecutiveDelta2 (q,o2)) in ( rng Ls) by A22, A23, A31, A43, FUNCT_1:def 3;

                then

                 A60: h2 c= f by A43, ZFMISC_1: 74;

                

                 A61: ( ConsecutiveSet2 (A,o3)) c= ( ConsecutiveSet2 (A,o2)) by A59, Th21;

                then

                reconsider z9 = z as Element of ( ConsecutiveSet2 (A,o2)) by A42;

                 [y, z] in ( dom h2) by A51, A42, A46, A61, ZFMISC_1: 87;

                then

                 A62: (f . (y,z)) = (h2 . (y9,z9)) by A60, GRFUNC_1: 2;

                ( ConsecutiveSet2 (A,o1)) c= ( ConsecutiveSet2 (A,o3)) by A52, Th21;

                then

                 A63: ( ConsecutiveSet2 (A,o1)) c= ( ConsecutiveSet2 (A,o2)) by A61;

                then

                reconsider x9 = x as Element of ( ConsecutiveSet2 (A,o2)) by A37;

                 [x, y] in ( dom h2) by A37, A51, A46, A63, ZFMISC_1: 87;

                then

                 A64: (f . (x,y)) = (h2 . (x9,y9)) by A60, GRFUNC_1: 2;

                 [x, z] in ( dom h2) by A37, A42, A46, A61, A63, ZFMISC_1: 87;

                then (f . (x,z)) = (h2 . (x9,z9)) by A60, GRFUNC_1: 2;

                hence thesis by A44, A64, A62;

              end;

            end;

          end;

            suppose

             A65: o3 c= o1;

            then

             A66: ( ConsecutiveSet2 (A,o3)) c= ( ConsecutiveSet2 (A,o1)) by Th21;

            thus ((f . (x,y)) "\/" (f . (y,z))) >= (f . (x,z))

            proof

              per cases ;

                suppose

                 A67: o1 c= o2;

                reconsider y9 = y as Element of ( ConsecutiveSet2 (A,o2)) by A23, A29, A31, A32;

                ( ConsecutiveDelta2 (q,o2)) in ( rng Ls) by A22, A23, A31, A43, FUNCT_1:def 3;

                then

                 A68: h2 c= f by A43, ZFMISC_1: 74;

                

                 A69: ( ConsecutiveSet2 (A,o1)) c= ( ConsecutiveSet2 (A,o2)) by A67, Th21;

                then

                reconsider x9 = x as Element of ( ConsecutiveSet2 (A,o2)) by A37;

                 [x, y] in ( dom h2) by A37, A51, A46, A69, ZFMISC_1: 87;

                then

                 A70: (f . (x,y)) = (h2 . (x9,y9)) by A68, GRFUNC_1: 2;

                ( ConsecutiveSet2 (A,o3)) c= ( ConsecutiveSet2 (A,o1)) by A65, Th21;

                then

                 A71: ( ConsecutiveSet2 (A,o3)) c= ( ConsecutiveSet2 (A,o2)) by A69;

                then

                reconsider z9 = z as Element of ( ConsecutiveSet2 (A,o2)) by A42;

                 [y, z] in ( dom h2) by A51, A42, A46, A71, ZFMISC_1: 87;

                then

                 A72: (f . (y,z)) = (h2 . (y9,z9)) by A68, GRFUNC_1: 2;

                 [x, z] in ( dom h2) by A37, A42, A46, A69, A71, ZFMISC_1: 87;

                then (f . (x,z)) = (h2 . (x9,z9)) by A68, GRFUNC_1: 2;

                hence thesis by A44, A70, A72;

              end;

                suppose

                 A73: o2 c= o1;

                reconsider x9 = x as Element of ( ConsecutiveSet2 (A,o1)) by A23, A25, A27, A28;

                reconsider z9 = z as Element of ( ConsecutiveSet2 (A,o1)) by A42, A66;

                ( ConsecutiveDelta2 (q,o1)) in ( rng Ls) by A22, A23, A27, A47, FUNCT_1:def 3;

                then

                 A74: h1 c= f by A47, ZFMISC_1: 74;

                

                 A75: ( ConsecutiveSet2 (A,o2)) c= ( ConsecutiveSet2 (A,o1)) by A73, Th21;

                then

                reconsider y9 = y as Element of ( ConsecutiveSet2 (A,o1)) by A51;

                 [x, y] in ( dom h1) by A37, A51, A50, A75, ZFMISC_1: 87;

                then

                 A76: (f . (x,y)) = (h1 . (x9,y9)) by A74, GRFUNC_1: 2;

                 [x, z] in ( dom h1) by A37, A42, A50, A66, ZFMISC_1: 87;

                then

                 A77: (f . (x,z)) = (h1 . (x9,z9)) by A74, GRFUNC_1: 2;

                 [y, z] in ( dom h1) by A51, A42, A50, A66, A75, ZFMISC_1: 87;

                then (f . (y,z)) = (h1 . (y9,z9)) by A74, GRFUNC_1: 2;

                hence thesis by A48, A76, A77;

              end;

            end;

          end;

        end;

        hence thesis by A19, A22, Th20;

      end;

      

       A78: X[ 0 ]

      proof

        assume 0 c= ( DistEsti d);

        let x,y,z be Element of ( ConsecutiveSet2 (A, 0 ));

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

        ( ConsecutiveDelta2 (q, 0 )) = d & (d . (x9,z9)) <= ((d . (x9,y9)) "\/" (d . (y9,z9))) by A3, Th18;

        hence (( ConsecutiveDelta2 (q, 0 )) . (x,z)) <= ((( ConsecutiveDelta2 (q, 0 )) . (x,y)) "\/" (( ConsecutiveDelta2 (q, 0 )) . (y,z)));

      end;

      for O be Ordinal holds X[O] from ORDINAL2:sch 1( A78, A4, A18);

      hence thesis;

    end;

    theorem :: LATTICE8:28

    for A be non empty set holds for L be lower-bounded modular LATTICE holds for d be distance_function of A, L holds for O be Ordinal holds for q be QuadrSeq of d st O c= ( DistEsti d) holds ( ConsecutiveDelta2 (q,O)) is distance_function of ( ConsecutiveSet2 (A,O)), L by Th25, Th26, Th27;

    definition

      let A be non empty set;

      let L be lower-bounded LATTICE;

      let d be BiFunction of A, L;

      :: LATTICE8:def8

      func NextSet2 (d) -> set equals ( ConsecutiveSet2 (A,( DistEsti d)));

      correctness ;

    end

    registration

      let A be non empty set;

      let L be lower-bounded LATTICE;

      let d be BiFunction of A, L;

      cluster ( NextSet2 d) -> non empty;

      coherence ;

    end

    definition

      let A be non empty set;

      let L be lower-bounded LATTICE;

      let d be BiFunction of A, L;

      let q be QuadrSeq of d;

      :: LATTICE8:def9

      func NextDelta2 (q) -> set equals ( ConsecutiveDelta2 (q,( DistEsti d)));

      correctness ;

    end

    definition

      let A be non empty set;

      let L be lower-bounded modular LATTICE;

      let d be distance_function of A, L;

      let q be QuadrSeq of d;

      :: original: NextDelta2

      redefine

      func NextDelta2 (q) -> distance_function of ( NextSet2 d), L ;

      coherence by Th25, Th26, Th27;

    end

    definition

      let A be non empty set;

      let L be lower-bounded LATTICE;

      let d be distance_function of A, L;

      let Aq be non empty set;

      let dq be distance_function of Aq, L;

      :: LATTICE8:def10

      pred Aq,dq is_extension2_of A,d means ex q be QuadrSeq of d st Aq = ( NextSet2 d) & dq = ( NextDelta2 q);

    end

    theorem :: LATTICE8:29

    

     Th29: for A be non empty set holds for L be lower-bounded LATTICE holds for d be distance_function of A, L holds for Aq be non empty set holds for dq be distance_function of Aq, L st (Aq,dq) is_extension2_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 be Element of Aq st (dq . (x,z1)) = a & (dq . (z1,z2)) = (((d . (x,y)) "\/" a) "/\" b) & (dq . (z2,y)) = a

    proof

      let A be non empty set;

      let L be lower-bounded LATTICE;

      let d be distance_function of A, L;

      let Aq be non empty set;

      let dq be distance_function of Aq, L;

      assume (Aq,dq) is_extension2_of (A,d);

      then

      consider q be QuadrSeq of d such that

       A1: Aq = ( NextSet2 d) and

       A2: dq = ( NextDelta2 q);

      let x,y be Element of A;

      let a,b be Element of L;

      

       A3: ( 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 LATTICE5:def 13;

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

      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) = ( Quadr2 (q,o)) by A4, Def6;

      then

       A7: x = (( Quadr2 (q,o)) `1_4 ) by A5;

      

       A8: b = (( Quadr2 (q,o)) `4_4 ) by A5, A6;

      

       A9: y = (( Quadr2 (q,o)) `2_4 ) by A5, A6;

      reconsider B = ( ConsecutiveSet2 (A,o)) as non empty set;

       {B} in { {B}, { {B}}} by TARSKI:def 2;

      then

       A10: {B} in (B \/ { {B}, { {B}}}) by XBOOLE_0:def 3;

      o in ( DistEsti d) by A4, LATTICE5: 25;

      then

       A11: ( succ o) c= ( DistEsti d) by ORDINAL1: 21;

      then

       A12: ( ConsecutiveDelta2 (q,( succ o))) c= ( ConsecutiveDelta2 (q,( DistEsti d))) by Th24;

      reconsider cd = ( ConsecutiveDelta2 (q,o)) as BiFunction of B, L;

      reconsider Q = ( Quadr2 (q,o)) as Element of [:B, B, the carrier of L, the carrier of L:];

      

       A13: { {B}} in { {B}, { {B}}} by TARSKI:def 2;

      then

       A14: { {B}} in ( new_set2 B) by XBOOLE_0:def 3;

      ( ConsecutiveSet2 (A,( succ o))) = ( new_set2 B) by Th15;

      then ( new_set2 B) c= ( ConsecutiveSet2 (A,( DistEsti d))) by A11, Th21;

      then

      reconsider z1 = {B}, z2 = { {B}} as Element of Aq by A1, A10, A14;

      take z1, z2;

      

       A15: cd is zeroed by Th25;

      A c= B by Th17;

      then

      reconsider xo = x, yo = y as Element of B;

      

       A16: B c= ( new_set2 B) by XBOOLE_1: 7;

      reconsider x1 = xo, y1 = yo as Element of ( new_set2 B) by A16;

      

       A17: ( ConsecutiveDelta2 (q,( succ o))) = ( new_bi_fun2 (( BiFun (( ConsecutiveDelta2 (q,o)),( ConsecutiveSet2 (A,o)),L)),( Quadr2 (q,o)))) by Th19

      .= ( new_bi_fun2 (cd,Q)) by LATTICE5:def 15;

      ( dom d) = [:A, A:] by FUNCT_2:def 1;

      then

       A18: [xo, yo] in ( dom d) by ZFMISC_1: 87;

      d c= cd by Th23;

      then

       A19: (cd . (xo,yo)) = (d . (x,y)) by A18, GRFUNC_1: 2;

      

       A20: a = (( Quadr2 (q,o)) `3_4 ) by A5, A6;

      

       A21: ( dom ( new_bi_fun2 (cd,Q))) = [:( new_set2 B), ( new_set2 B):] by FUNCT_2:def 1;

      then [x1, {B}] in ( dom ( new_bi_fun2 (cd,Q))) by A10, ZFMISC_1: 87;

      

      hence (dq . (x,z1)) = (( new_bi_fun2 (cd,Q)) . (x1, {B})) by A2, A12, A17, GRFUNC_1: 2

      .= ((cd . (xo,xo)) "\/" a) by A7, A20, Def4

      .= (( Bottom L) "\/" a) by A15

      .= a by WAYBEL_1: 3;

       [ {B}, { {B}}] in ( dom ( new_bi_fun2 (cd,Q))) by A10, A14, A21, ZFMISC_1: 87;

      

      hence (dq . (z1,z2)) = (( new_bi_fun2 (cd,Q)) . ( {B}, { {B}})) by A2, A12, A17, GRFUNC_1: 2

      .= (((d . (x,y)) "\/" a) "/\" b) by A7, A9, A20, A8, A19, Def4;

       { {B}} in (B \/ { {B}, { {B}}}) by A13, XBOOLE_0:def 3;

      then [ { {B}}, y1] in ( dom ( new_bi_fun2 (cd,Q))) by A21, ZFMISC_1: 87;

      

      hence (dq . (z2,y)) = (( new_bi_fun2 (cd,Q)) . ( { {B}},y1)) by A2, A12, A17, GRFUNC_1: 2

      .= ((cd . (yo,yo)) "\/" a) by A9, A20, Def4

      .= (( Bottom L) "\/" a) by A15

      .= a by WAYBEL_1: 3;

    end;

    definition

      let A be non empty set;

      let L be lower-bounded modular LATTICE;

      let d be distance_function of A, L;

      :: LATTICE8:def11

      mode ExtensionSeq2 of A,d -> Function means

      : Def11: ( 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_extension2_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_extension2_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_extension2_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_extension2_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_extension2_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_extension2_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_extension2_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_extension2_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_extension2_of (A1,d1) & (f . (k + 1)) = [A1, d1]

          proof

            set Q = the QuadrSeq of dq;

            set AQ = ( NextSet2 dq);

            take Aq, dq;

            set DQ = ( NextDelta2 Q);

            take AQ, DQ;

            thus (AQ,DQ) is_extension2_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_extension2_of (A9,d9) & (f . 0 ) = [A9, d9]

        proof

          set Aq = ( NextSet2 d);

          set q = the QuadrSeq of d;

          take A, d;

          consider dq be distance_function of Aq, L such that

           A9: dq = ( NextDelta2 q);

          take Aq, dq;

          thus (Aq,dq) is_extension2_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 :: LATTICE8:30

    

     Th30: for A be non empty set holds for L be lower-bounded modular LATTICE holds for d be distance_function of A, L holds for S be ExtensionSeq2 of A, d holds for k,l be Nat st k <= l holds ((S . k) `1 ) c= ((S . l) `1 )

    proof

      let A be non empty set;

      let L be lower-bounded modular LATTICE;

      let d be distance_function of A, L;

      let S be ExtensionSeq2 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_extension2_of (A9,d9) and

           A6: (S . i) = [A9, d9] and

           A7: (S . (i + 1)) = [Aq, dq] by Def11;

          

           A8: ((S . i) `1 ) c= ( ConsecutiveSet2 (A9,( DistEsti d9))) by Th17, A6;

          ex q be QuadrSeq of d9 st Aq = ( NextSet2 d9) & dq = ( NextDelta2 q) by A5;

          then ( [Aq, dq] `1 ) = ( ConsecutiveSet2 (A9,( DistEsti d9)));

          hence thesis by A2, A4, A8, A7;

        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 :: LATTICE8:31

    

     Th31: for A be non empty set holds for L be lower-bounded modular LATTICE holds for d be distance_function of A, L holds for S be ExtensionSeq2 of A, d holds for k,l be Nat st k <= l holds ((S . k) `2 ) c= ((S . l) `2 )

    proof

      let A be non empty set;

      let L be lower-bounded modular LATTICE;

      let d be distance_function of A, L;

      let S be ExtensionSeq2 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_extension2_of (A9,d9) and

           A6: (S . i) = [A9, d9] and

           A7: (S . (i + 1)) = [Aq, dq] by Def11;

          consider q be QuadrSeq of d9 such that Aq = ( NextSet2 d9) and

           A8: dq = ( NextDelta2 q) by A5;

          

           A9: ((S . i) `2 ) c= ( ConsecutiveDelta2 (q,( DistEsti d9))) by Th23, A6;

          ( [Aq, dq] `2 ) = ( ConsecutiveDelta2 (q,( DistEsti d9))) by A8;

          hence thesis by A2, A4, A9, A7;

        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;

    theorem :: LATTICE8:32

    

     Th32: for L be lower-bounded modular LATTICE holds for S be ExtensionSeq2 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 L be lower-bounded modular LATTICE;

      let S be ExtensionSeq2 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, Th31;

        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_extension2_of (A9,d9) and

         A8: (S . j) = [A9, d9] and (S . (j + 1)) = [Aq, dq] by Def11;

        

         A9: A9 = ( [A9, d9] `1 );

        A9 in the set of all ((S . i) `1 ) where i be Element of NAT by A9, A8;

        then ( dom d9) = [:A9, A9:] & A9 c= FS by A1, FUNCT_2:def 1, ZFMISC_1: 74;

        then

         A10: ( rng d9) c= A & ( dom d9) c= [:FS, FS:] by ZFMISC_1: 96;

        z = d9 by A7, A8;

        hence thesis by A10, PARTFUN1:def 3;

      end;

      then FD in ( PFuncs ( [:FS, FS:],A)) by A6, TREES_2: 40;

      then

       A11: 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 );

      

       A12: 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

           A13: x = [:J, J:] and

           A14: J in X;

          ex j be Element of NAT st J = ((S . j) `1 ) by A14;

          hence thesis by A13;

        end;

        let x be object;

        assume x in PP;

        then

        consider j be Element of NAT such that

         A15: x = [:((S . j) `1 ), ((S . j) `1 ):];

        ((S . j) `1 ) in X;

        hence thesis by A15;

      end;

      reconsider FD as Function by A11;

      

       A16: for x be object st x in NAT holds ex y be object st X[x, y];

      consider F be Function such that

       A17: ( dom F) = NAT and

       A18: for x be object st x in NAT holds X[x, (F . x)] from CLASSES1:sch 1( A16);

      

       A19: ( 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

           A20: j in ( dom F) and

           A21: (F . j) = x by FUNCT_1:def 3;

          reconsider j as Element of NAT by A17, A20;

          x = ((S . j) `2 ) by A18, A21;

          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

         A22: x = ((S . j) `2 );

        x = (F . j) by A18, A22;

        hence thesis by A17, 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 A17;

        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_extension2_of (A1,d1) and

         A23: (S . j) = [A1, d1] and (S . (j + 1)) = [Aq1, dq1] by Def11;

        ( [A1, d1] `2 ) = d1;

        hence thesis by A18, A23;

      end;

      then

      reconsider F as Function-yielding Function;

      

       A24: ( 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

           A25: j in ( dom ( doms F)) and

           A26: x = (( doms F) . j) by FUNCT_1:def 3;

          

           A27: j in ( dom F) by A25, FUNCT_6: 59;

          reconsider j as Element of NAT by A17, A25, 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_extension2_of (A1,d1) and

           A28: (S . j) = [A1, d1] and (S . (j + 1)) = [Aq1, dq1] by Def11;

          

           A29: ( [A1, d1] `2 ) = d1;

          x = ( dom (F . j)) by A26, A27, FUNCT_6: 22

          .= ( dom d1) by A18, A29, A28

          .= [:((S . j) `1 ), ((S . j) `1 ):] by A28, FUNCT_2:def 1;

          hence thesis;

        end;

        let x be object;

        assume x in PP;

        then

        consider j be Element of NAT such that

         A30: 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_extension2_of (A1,d1) and

         A31: (S . j) = [A1, d1] and (S . (j + 1)) = [Aq1, dq1] by Def11;

        

         A32: ( [A1, d1] `2 ) = d1;

        j in NAT ;

        then

         A33: j in ( dom ( doms F)) by A17, FUNCT_6: 59;

        x = ( dom d1) by A30, A31, FUNCT_2:def 1

        .= ( dom (F . j)) by A18, A32, A31

        .= (( doms F) . j) by A17, FUNCT_6: 22;

        hence thesis by A33, FUNCT_1:def 3;

      end;

      now

        let x,y be set;

        assume that

         A34: x in X and

         A35: y in X;

        consider k be Element of NAT such that

         A36: x = ((S . k) `1 ) by A34;

        consider l be Element of NAT such that

         A37: y = ((S . l) `1 ) by A35;

        k <= l or l <= k;

        then x c= y or y c= x by A36, A37, Th30;

        hence (x,y) are_c=-comparable ;

      end;

      then X is c=-linear;

      

      then [:FS, FS:] = ( union ( rng ( doms F))) by A1, A24, A12, LATTICE5: 3

      .= ( dom FD) by A19, LATTICE5: 1;

      then

      reconsider FD as BiFunction of FS, L by A11, FUNCT_2:def 1, RELSET_1: 4;

      

       A38: FD is symmetric

      proof

        let x,y be Element of FS;

        consider x1 be set such that

         A39: x in x1 and

         A40: x1 in X by A1, TARSKI:def 4;

        consider k be Element of NAT such that

         A41: x1 = ((S . k) `1 ) by A40;

        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_extension2_of (A1,d1) and

         A42: (S . k) = [A1, d1] and (S . (k + 1)) = [Aq1, dq1] by Def11;

        

         A43: ( [A1, d1] `1 ) = A1;

        

         A44: x in A1 by A39, A41, A42;

        ( [A1, d1] `2 ) = d1;

        then d1 in the set of all ((S . i) `2 ) where i be Element of NAT by A42;

        then

         A45: d1 c= FD by ZFMISC_1: 74;

        consider y1 be set such that

         A46: y in y1 and

         A47: y1 in X by A1, TARSKI:def 4;

        consider l be Element of NAT such that

         A48: y1 = ((S . l) `1 ) by A47;

        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_extension2_of (A2,d2) and

         A49: (S . l) = [A2, d2] and (S . (l + 1)) = [Aq2, dq2] by Def11;

        

         A50: ( [A2, d2] `1 ) = A2;

        

         A51: y in A2 by A46, A48, A49;

        ( [A2, d2] `2 ) = d2;

        then d2 in the set of all ((S . i) `2 ) where i be Element of NAT by A49;

        then

         A52: d2 c= FD by ZFMISC_1: 74;

        per cases ;

          suppose k <= l;

          then A1 c= A2 by A43, A50, Th30, A42, A49;

          then

          reconsider x9 = x, y9 = y as Element of A2 by A44, A46, A48, A49;

          

           A53: ( dom d2) = [:A2, A2:] by FUNCT_2:def 1;

          

          hence (FD . (x,y)) = (d2 . [x9, y9]) by A52, GRFUNC_1: 2

          .= (d2 . (x9,y9))

          .= (d2 . (y9,x9)) by LATTICE5:def 5

          .= (FD . [y9, x9]) by A52, A53, GRFUNC_1: 2

          .= (FD . (y,x));

        end;

          suppose l <= k;

          then A2 c= A1 by A43, A50, Th30, A42, A49;

          then

          reconsider x9 = x, y9 = y as Element of A1 by A39, A41, A42, A51;

          

           A54: ( dom d1) = [:A1, A1:] by FUNCT_2:def 1;

          

          hence (FD . (x,y)) = (d1 . [x9, y9]) by A45, GRFUNC_1: 2

          .= (d1 . (x9,y9))

          .= (d1 . (y9,x9)) by LATTICE5:def 5

          .= (FD . [y9, x9]) by A45, A54, GRFUNC_1: 2

          .= (FD . (y,x));

        end;

      end;

      

       A55: FD is u.t.i.

      proof

        let x,y,z be Element of FS;

        consider x1 be set such that

         A56: x in x1 and

         A57: x1 in X by A1, TARSKI:def 4;

        consider k be Element of NAT such that

         A58: x1 = ((S . k) `1 ) by A57;

        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_extension2_of (A1,d1) and

         A59: (S . k) = [A1, d1] and (S . (k + 1)) = [Aq1, dq1] by Def11;

        

         A60: ( [A1, d1] `1 ) = A1;

        

         A61: x in A1 by A56, A58, A59;

        ( [A1, d1] `2 ) = d1;

        then d1 in the set of all ((S . i) `2 ) where i be Element of NAT by A59;

        then

         A62: d1 c= FD by ZFMISC_1: 74;

        

         A63: ( dom d1) = [:A1, A1:] by FUNCT_2:def 1;

        consider y1 be set such that

         A64: y in y1 and

         A65: y1 in X by A1, TARSKI:def 4;

        consider l be Element of NAT such that

         A66: y1 = ((S . l) `1 ) by A65;

        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_extension2_of (A2,d2) and

         A67: (S . l) = [A2, d2] and (S . (l + 1)) = [Aq2, dq2] by Def11;

        

         A68: ( [A2, d2] `1 ) = A2;

        

         A69: y in A2 by A64, A66, A67;

        ( [A2, d2] `2 ) = d2;

        then d2 in the set of all ((S . i) `2 ) where i be Element of NAT by A67;

        then

         A70: d2 c= FD by ZFMISC_1: 74;

        

         A71: ( dom d2) = [:A2, A2:] by FUNCT_2:def 1;

        consider z1 be set such that

         A72: z in z1 and

         A73: z1 in X by A1, TARSKI:def 4;

        consider n be Element of NAT such that

         A74: z1 = ((S . n) `1 ) by A73;

        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_extension2_of (A3,d3) and

         A75: (S . n) = [A3, d3] and (S . (n + 1)) = [Aq3, dq3] by Def11;

        

         A76: ( [A3, d3] `1 ) = A3;

        

         A77: z in A3 by A72, A74, A75;

        ( [A3, d3] `2 ) = d3;

        then d3 in the set of all ((S . i) `2 ) where i be Element of NAT by A75;

        then

         A78: d3 c= FD by ZFMISC_1: 74;

        

         A79: ( dom d3) = [:A3, A3:] by FUNCT_2:def 1;

        per cases ;

          suppose k <= l;

          then

           A80: A1 c= A2 by A60, A68, Th30, A59, A67;

          thus ((FD . (x,y)) "\/" (FD . (y,z))) >= (FD . (x,z))

          proof

            per cases ;

              suppose l <= n;

              then

               A81: A2 c= A3 by A68, A76, Th30, A67, A75;

              then A1 c= A3 by A80;

              then

              reconsider x9 = x, y9 = y, z9 = z as Element of A3 by A61, A69, A72, A74, A75, A81;

              

               A82: (FD . (y,z)) = (d3 . [y9, z9]) by A78, A79, GRFUNC_1: 2

              .= (d3 . (y9,z9));

              

               A83: (FD . (x,z)) = (d3 . [x9, z9]) by A78, A79, GRFUNC_1: 2

              .= (d3 . (x9,z9));

              (FD . (x,y)) = (d3 . [x9, y9]) by A78, A79, GRFUNC_1: 2

              .= (d3 . (x9,y9));

              hence thesis by A82, A83, LATTICE5:def 7;

            end;

              suppose n <= l;

              then A3 c= A2 by A68, A76, Th30, A67, A75;

              then

              reconsider x9 = x, y9 = y, z9 = z as Element of A2 by A61, A64, A66, A67, A77, A80;

              

               A84: (FD . (y,z)) = (d2 . [y9, z9]) by A70, A71, GRFUNC_1: 2

              .= (d2 . (y9,z9));

              

               A85: (FD . (x,z)) = (d2 . [x9, z9]) by A70, A71, GRFUNC_1: 2

              .= (d2 . (x9,z9));

              (FD . (x,y)) = (d2 . [x9, y9]) by A70, A71, GRFUNC_1: 2

              .= (d2 . (x9,y9));

              hence thesis by A84, A85, LATTICE5:def 7;

            end;

          end;

        end;

          suppose l <= k;

          then

           A86: A2 c= A1 by A60, A68, Th30, A59, A67;

          thus ((FD . (x,y)) "\/" (FD . (y,z))) >= (FD . (x,z))

          proof

            per cases ;

              suppose k <= n;

              then

               A87: A1 c= A3 by A60, A76, Th30, A59, A75;

              then A2 c= A3 by A86;

              then

              reconsider x9 = x, y9 = y, z9 = z as Element of A3 by A61, A69, A72, A74, A75, A87;

              

               A88: (FD . (y,z)) = (d3 . [y9, z9]) by A78, A79, GRFUNC_1: 2

              .= (d3 . (y9,z9));

              

               A89: (FD . (x,z)) = (d3 . [x9, z9]) by A78, A79, GRFUNC_1: 2

              .= (d3 . (x9,z9));

              (FD . (x,y)) = (d3 . [x9, y9]) by A78, A79, GRFUNC_1: 2

              .= (d3 . (x9,y9));

              hence thesis by A88, A89, LATTICE5:def 7;

            end;

              suppose n <= k;

              then A3 c= A1 by A60, A76, Th30, A59, A75;

              then

              reconsider x9 = x, y9 = y, z9 = z as Element of A1 by A56, A58, A59, A69, A77, A86;

              

               A90: (FD . (y,z)) = (d1 . [y9, z9]) by A62, A63, GRFUNC_1: 2

              .= (d1 . (y9,z9));

              

               A91: (FD . (x,z)) = (d1 . [x9, z9]) by A62, A63, GRFUNC_1: 2

              .= (d1 . (x9,z9));

              (FD . (x,y)) = (d1 . [x9, y9]) by A62, A63, GRFUNC_1: 2

              .= (d1 . (x9,y9));

              hence thesis by A90, A91, LATTICE5:def 7;

            end;

          end;

        end;

      end;

      FD is zeroed

      proof

        let x be Element of FS;

        consider y be set such that

         A92: x in y and

         A93: y in X by A1, TARSKI:def 4;

        consider j be Element of NAT such that

         A94: y = ((S . j) `1 ) by A93;

        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_extension2_of (A1,d1) and

         A95: (S . j) = [A1, d1] and (S . (j + 1)) = [Aq1, dq1] by Def11;

        ( [A1, d1] `2 ) = d1;

        then d1 in the set of all ((S . i) `2 ) where i be Element of NAT by A95;

        then

         A96: d1 c= FD by ZFMISC_1: 74;

        reconsider x9 = x as Element of A1 by A92, A94, A95;

        ( dom d1) = [:A1, A1:] by FUNCT_2:def 1;

        

        hence (FD . (x,x)) = (d1 . [x9, x9]) by A96, GRFUNC_1: 2

        .= (d1 . (x9,x9))

        .= ( Bottom L) by LATTICE5:def 6;

      end;

      hence thesis by A38, A55;

    end;

    theorem :: LATTICE8:33

    

     Th33: for L be lower-bounded modular LATTICE holds for S be ExtensionSeq2 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 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 be Element of FS st (FD . (x,z1)) = a & (FD . (z1,z2)) = (((FD . (x,y)) "\/" a) "/\" b) & (FD . (z2,y)) = a

    proof

      let L be lower-bounded modular LATTICE;

      let S be ExtensionSeq2 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_extension2_of (A1,d1) and

       A8: (S . k) = [A1, d1] and

       A9: (S . (k + 1)) = [Aq1, dq1] by Def11;

      

       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_extension2_of (A2,d2) and

       A20: (S . l) = [A2, d2] and

       A21: (S . (l + 1)) = [Aq2, dq2] by Def11;

      

       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, Th30, A8, A20;

        then

        reconsider x9 = x, y9 = y as Element of A2 by A11, A16, A18, A20;

        A2 c= Aq2 by A22, A25, Th30, 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

         A28: (FD . (x,y)) = (d2 . [x9, y9]) by A24, GRFUNC_1: 2

        .= (d2 . (x9,y9));

        then

        consider z1,z2 be Element of Aq2 such that

         A29: (dq2 . (x,z1)) = a and

         A30: (dq2 . (z1,z2)) = (((d2 . (x9,y9)) "\/" a) "/\" b) and

         A31: (dq2 . (z2,y)) = a by A3, A19, Th29;

        reconsider z19 = z1, z29 = z2 as Element of FS by A26;

        take z19, z29;

        

         A32: ( dom dq2) = [:Aq2, Aq2:] by FUNCT_2:def 1;

        

        hence (FD . (x,z19)) = (dq2 . [x99, z1]) by A27, GRFUNC_1: 2

        .= a by A29;

        

        thus (FD . (z19,z29)) = (dq2 . [z1, z2]) by A27, A32, GRFUNC_1: 2

        .= (((FD . (x,y)) "\/" a) "/\" b) by A28, A30;

        

        thus (FD . (z29,y)) = (dq2 . [z2, y99]) by A27, A32, GRFUNC_1: 2

        .= a by A31;

      end;

        suppose l <= k;

        then A2 c= A1 by A10, A22, Th30, A8, A20;

        then

        reconsider x9 = x, y9 = y as Element of A1 by A4, A6, A8, A23;

        A1 c= Aq1 by A10, A13, Th30, 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

         A33: (FD . (x,y)) = (d1 . [x9, y9]) by A12, GRFUNC_1: 2

        .= (d1 . (x9,y9));

        then

        consider z1,z2 be Element of Aq1 such that

         A34: (dq1 . (x,z1)) = a and

         A35: (dq1 . (z1,z2)) = (((d1 . (x9,y9)) "\/" a) "/\" b) and

         A36: (dq1 . (z2,y)) = a by A3, A7, Th29;

        reconsider z19 = z1, z29 = z2 as Element of FS by A14;

        take z19, z29;

        

         A37: ( dom dq1) = [:Aq1, Aq1:] by FUNCT_2:def 1;

        

        hence (FD . (x,z19)) = (dq1 . [x99, z1]) by A15, GRFUNC_1: 2

        .= a by A34;

        

        thus (FD . (z19,z29)) = (dq1 . [z1, z2]) by A15, A37, GRFUNC_1: 2

        .= (((FD . (x,y)) "\/" a) "/\" b) by A33, A35;

        

        thus (FD . (z29,y)) = (dq1 . [z2, y99]) by A15, A37, GRFUNC_1: 2

        .= a by A36;

      end;

    end;

    

     Lm3: for m be Element of NAT st m in ( Seg 4) holds (m = 1 or m = 2 or m = 3 or m = 4)

    proof

      let m be Element of NAT ;

      assume

       A1: m in ( Seg 4);

      then m <= 4 by FINSEQ_1: 1;

      then m = 0 or ... or m = 4 by NAT_1: 60;

      hence thesis by A1, FINSEQ_1: 1;

    end;

    

     Lm4: for j be Nat st 1 <= j & j < 4 holds j = 1 or j = 2 or j = 3

    proof

      let j be Nat;

      assume that

       A1: 1 <= j and

       A2: j < 4;

      j < (3 + 1) by A2;

      then j <= 3 by NAT_1: 13;

      then j = 0 or ... or j = 3 by NAT_1: 60;

      hence thesis by A1;

    end;

    theorem :: LATTICE8:34

    

     Th34: for L be lower-bounded modular LATTICE holds for S be ExtensionSeq2 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 e1,e2 be Equivalence_Relation of FS holds for 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) = (2 + 2) & (x,y) are_joint_by (F,e1,e2)

    proof

      let L be lower-bounded modular LATTICE;

      let S be ExtensionSeq2 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 e1,e2 be Equivalence_Relation of FS;

      let 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: the carrier of ( Image f) = ( rng f) by YELLOW_0:def 15;

      then

      consider a be object such that

       A7: a in ( dom f) and

       A8: e1 = (f . a) by A3, FUNCT_1:def 3;

      consider b be object such that

       A9: b in ( dom f) and

       A10: e2 = (f . b) by A4, A6, FUNCT_1:def 3;

      reconsider a, b as Element of L by A7, A9;

      reconsider a, b as Element of L;

      consider e be Equivalence_Relation of FS such that

       A11: e = (f . (a "\/" b)) and

       A12: for u,v be Element of FS holds [u, v] in e iff (FD . (u,v)) <= (a "\/" b) by A1, LATTICE5:def 8;

      consider e29 be Equivalence_Relation of FS such that

       A13: e29 = (f . b) and

       A14: for u,v be Element of FS holds [u, v] in e29 iff (FD . (u,v)) <= b by A1, LATTICE5:def 8;

      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, LATTICE5:def 8;

      ( field (e1 "\/" e2)) = FS by ORDERS_1: 12;

      then

      reconsider u = x, v = y as Element of FS by A5, RELAT_1: 15;

      

       A17: ( Seg 4) = { n where n be Nat : 1 <= n & n <= 4 } by FINSEQ_1:def 1;

      then

       A18: 1 in ( Seg 4);

      e = ((f . a) "\/" (f . b)) by A11, WAYBEL_6: 2

      .= (e1 "\/" e2) by A8, A10, LATTICE5: 10;

      then

       A19: (FD . (u,v)) <= (a "\/" b) by A5, A12;

      then

      consider z1,z2 be Element of FS such that

       A20: (FD . (u,z1)) = a and

       A21: (FD . (z1,z2)) = (((FD . (u,v)) "\/" a) "/\" b) and

       A22: (FD . (z2,v)) = a by A2, Th33;

      defpred P[ set, object] means ($1 = 1 implies $2 = u) & ($1 = 2 implies $2 = z1) & ($1 = 3 implies $2 = z2) & ($1 = 4 implies $2 = v);

      

       A23: for m be Nat st m in ( Seg 4) holds ex w be object st P[m, w]

      proof

        let m be Nat;

        assume

         A24: m in ( Seg 4);

        per cases by A24, Lm3;

          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 y;

          thus thesis by A28;

        end;

      end;

      ex p be FinSequence st ( dom p) = ( Seg 4) & for k be Nat st k in ( Seg 4) holds P[k, (p . k)] from FINSEQ_1:sch 1( A23);

      then

      consider h be FinSequence such that

       A29: ( dom h) = ( Seg 4) and

       A30: for m be Nat st m in ( Seg 4) holds (m = 1 implies (h . m) = u) & (m = 2 implies (h . m) = z1) & (m = 3 implies (h . m) = z2) & (m = 4 implies (h . m) = v);

      

       A31: ( len h) = 4 by A29, FINSEQ_1:def 3;

      

       A32: 3 in ( Seg 4) by A17;

      

       A33: 4 in ( Seg 4) by A17;

      

       A34: 2 in ( Seg 4) by A17;

      ( 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;

        per cases by A29, A35, Lm3;

          suppose j = 1;

          then (h . j) = u by A30, A18;

          hence thesis by A36;

        end;

          suppose j = 2;

          then (h . j) = z1 by A30, A34;

          hence thesis by A36;

        end;

          suppose j = 3;

          then (h . j) = z2 by A30, A32;

          hence thesis by A36;

        end;

          suppose j = 4;

          then (h . j) = v by A30, A33;

          hence thesis by A36;

        end;

      end;

      then

      reconsider h as FinSequence of FS by FINSEQ_1:def 4;

      ( len h) <> 0 by A29, FINSEQ_1:def 3;

      then

      reconsider h as non empty FinSequence of FS;

      

       A37: (h . 1) = x by A30, A18;

      

       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

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

        per cases by A31, A39, Lm4;

          suppose

           A40: j = 1;

           [u, z1] in e19 by A16, A20;

          then [(h . 1), z1] in e19 by A30, A18;

          hence thesis by A8, A15, A30, A34, A40;

        end;

          suppose

           A41: j = 2;

          ((FD . (u,v)) "\/" a) <= ((a "\/" b) "\/" a) by A19, WAYBEL_1: 2;

          then ((FD . (u,v)) "\/" a) <= (b "\/" (a "\/" a)) by LATTICE3: 14;

          then ((FD . (u,v)) "\/" a) <= (b "\/" a) by YELLOW_5: 1;

          then (((FD . (u,v)) "\/" a) "/\" b) <= (b "/\" (b "\/" a)) by WAYBEL_1: 1;

          then (((FD . (u,v)) "\/" a) "/\" b) <= b by LATTICE3: 18;

          then [z1, z2] in e29 by A14, A21;

          then

           A42: [(h . 2), z2] in e29 by A30, A34;

          consider i be Element of NAT such that

           A43: i = 1;

          (2 * i) = j by A41, A43;

          hence thesis by A10, A13, A30, A32, A41, A42;

        end;

          suppose

           A44: j = 3;

           [z2, v] in e19 by A16, A22;

          then

           A45: [(h . 3), v] in e19 by A30, A32;

          consider i be Element of NAT such that

           A46: i = 1;

          ((2 * i) + 1) = j by A44, A46;

          hence thesis by A8, A15, A30, A33, A44, A45;

        end;

      end;

      take h;

      thus ( len h) = (2 + 2) by A29, FINSEQ_1:def 3;

      (h . ( len h)) = (h . 4) by A29, FINSEQ_1:def 3

      .= y by A30, A33;

      hence thesis by A37, A38;

    end;

    theorem :: LATTICE8:35

    

     Th35: for L be lower-bounded modular LATTICE holds L has_a_representation_of_type<= 2

    proof

      let L be lower-bounded modular LATTICE;

      set A = the carrier of L, D = ( BasicDF L);

      set S = the ExtensionSeq2 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 Def11;

      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 Th32;

      ( 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 e2 be Equivalence_Relation of FS such that

         A4: e2 = (f . b) and

         A5: for x,y be Element of FS holds [x, y] in e2 iff (FD . (x,y)) <= b by LATTICE5:def 8;

        consider e1 be Equivalence_Relation of FS such that

         A6: e1 = (f . a) and

         A7: for x,y be Element of FS holds [x, y] in e1 iff (FD . (x,y)) <= a by LATTICE5:def 8;

        consider e3 be Equivalence_Relation of FS such that

         A8: e3 = (f . (a "\/" b)) and

         A9: for x,y be Element of FS holds [x, y] in e3 iff (FD . (x,y)) <= (a "\/" b) by LATTICE5:def 8;

        

         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 A5, A12;

          then (FD . (x9,y9)) <= (b "\/" a) by A11, ORDERS_2: 3;

          hence [x, y] in e3 by A9;

        end;

        then

         A13: e2 c= e3;

        

         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: ( Seg 4) = { n where n be Nat : 1 <= n & n <= 4 } by FINSEQ_1:def 1;

          then

           A16: 3 in ( Seg 4);

          assume

           A17: [u, v] in e3;

          then

          reconsider x = u, y = v as Element of FS by A14, RELAT_1: 15;

          

           A18: (FD . (x,y)) <= (a "\/" b) by A9, A17;

          then

          consider z1,z2 be Element of FS such that

           A19: (FD . (x,z1)) = a and

           A20: (FD . (z1,z2)) = (((FD . (x,y)) "\/" a) "/\" b) and

           A21: (FD . (z2,y)) = a by Th33;

          

           A22: u in FS by A14, A17, 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 = y);

          

           A23: for m be Nat st m in ( Seg 4) holds ex w be object st P[m, w]

          proof

            let m be Nat;

            assume

             A24: m in ( Seg 4);

            per cases by A24, Lm3;

              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 y;

              thus thesis by A28;

            end;

          end;

          ex p be FinSequence st ( dom p) = ( Seg 4) & for k be Nat st k in ( Seg 4) holds P[k, (p . k)] from FINSEQ_1:sch 1( A23);

          then

          consider h be FinSequence such that

           A29: ( dom h) = ( Seg 4) and

           A30: for m be Nat st m in ( Seg 4) holds (m = 1 implies (h . m) = x) & (m = 2 implies (h . m) = z1) & (m = 3 implies (h . m) = z2) & (m = 4 implies (h . m) = y);

          

           A31: ( len h) = 4 by A29, FINSEQ_1:def 3;

          

           A32: 4 in ( Seg 4) by A15;

          

           A33: 1 in ( Seg 4) by A15;

          then

           A34: u = (h . 1) by A30;

          

           A35: 2 in ( Seg 4) by A15;

          

           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

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

            per cases by A31, A37, Lm4;

              suppose

               A38: j = 1;

               [x, z1] in e1 by A7, A19;

              then [(h . 1), z1] in e1 by A30, A33;

              then [(h . 1), (h . 2)] in e1 by A30, A35;

              hence thesis by A38, XBOOLE_0:def 3;

            end;

              suppose

               A39: j = 2;

              ((FD . (x,y)) "\/" a) <= ((a "\/" b) "\/" a) by A18, WAYBEL_1: 2;

              then ((FD . (x,y)) "\/" a) <= (b "\/" (a "\/" a)) by LATTICE3: 14;

              then ((FD . (x,y)) "\/" a) <= (b "\/" a) by YELLOW_5: 1;

              then (((FD . (x,y)) "\/" a) "/\" b) <= (b "/\" (b "\/" a)) by WAYBEL_1: 1;

              then (((FD . (x,y)) "\/" a) "/\" b) <= b by LATTICE3: 18;

              then [z1, z2] in e2 by A5, A20;

              then [(h . 2), z2] in e2 by A30, A35;

              then [(h . 2), (h . 3)] in e2 by A30, A16;

              hence thesis by A39, XBOOLE_0:def 3;

            end;

              suppose

               A40: j = 3;

               [z2, y] in e1 by A7, A21;

              then [(h . 3), y] in e1 by A30, A16;

              then [(h . 3), (h . 4)] in e1 by A30, A32;

              hence thesis by A40, XBOOLE_0:def 3;

            end;

          end;

          v = (h . 4) by A30, A32

          .= (h . ( len h)) by A29, FINSEQ_1:def 3;

          hence thesis by A22, A31, A34, A36, EQREL_1: 28;

        end;

        then

         A41: e3 c= (e1 "\/" e2);

        

         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 A7, A44;

          then (FD . (x9,y9)) <= (a "\/" b) by A43, ORDERS_2: 3;

          hence [x, y] in e3 by A9;

        end;

        then e1 c= e3;

        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 A6, A4, LATTICE5: 10

        .= (f . (a "\/" b)) by A8, 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 LATTICE5: 14;

      

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

      

       A47: ex e be Equivalence_Relation of FS st e in the carrier of ( Image f) & e <> ( id FS)

      proof

        

         A48: {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

         A49: (Aq9,dq9) is_extension2_of (A9,d9) and

         A50: (S . 0 ) = [A9, d9] and

         A51: (S . ( 0 + 1)) = [Aq9, dq9] by Def11;

        A9 = A & d9 = D by A2, A50, XTUPLE_0: 1;

        then

        consider q be QuadrSeq of D such that

         A52: Aq9 = ( NextSet2 D) and

         A53: dq9 = ( NextDelta2 q) by A49;

        ( ConsecutiveSet2 (A, {} )) = A by Th14;

        then

        reconsider Q = ( Quadr2 (q, {} )) as Element of [:A, A, the carrier of L, the carrier of L:];

        

         A54: ((S . 1) `2 ) in the set of all ((S . i) `2 ) where i be Element of NAT ;

        ( succ {} ) c= ( DistEsti D) by Th1;

        then {} in ( DistEsti D) by ORDINAL1: 21;

        then

         A55: {} in ( dom q) by LATTICE5: 25;

        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 LATTICE5:def 13;

        then

        consider u,v be Element of A, a,b be Element of L such that

         A56: (q . {} ) = [u, v, a, b] and (D . (u,v)) <= (a "\/" b);

        consider e be Equivalence_Relation of FS such that

         A57: e = (f . b) and

         A58: for x,y be Element of FS holds [x, y] in e iff (FD . (x,y)) <= b by LATTICE5:def 8;

        ( Quadr2 (q, {} )) = [u, v, a, b] by A55, A56, Def6;

        then

         A59: b = (Q `4_4 );

        ( [Aq9, dq9] `2 ) = ( NextDelta2 q) by A53;

        then

         A60: ( NextDelta2 q) c= FD by A54, A51, ZFMISC_1: 74;

        

         A61: { {A}} in { {A}, { {A}}} by TARSKI:def 2;

        then

         A62: { {A}} in (A \/ { {A}, { {A}}}) by XBOOLE_0:def 3;

        take e;

        e in ( rng f) by A46, A57, FUNCT_1:def 3;

        hence e in the carrier of ( Image f) by YELLOW_0:def 15;

        

         A63: ((S . 1) `1 ) in the set of all ((S . i) `1 ) where i be Element of NAT ;

        ( [Aq9, dq9] `1 ) = ( NextSet2 D) by A52;

        then

         A64: ( NextSet2 D) c= FS by A63, A51, ZFMISC_1: 74;

        ( new_set2 A) = ( new_set2 ( ConsecutiveSet2 (A, {} ))) by Th14

        .= ( ConsecutiveSet2 (A,( succ {} ))) by Th15;

        then ( new_set2 A) c= ( NextSet2 D) by Th1, Th21;

        then

         A65: ( new_set2 A) c= FS by A64;

        

         A66: { {A}} in ( new_set2 A) by A61, XBOOLE_0:def 3;

        

         A67: {A} in { {A}, { {A}}} by TARSKI:def 2;

        then {A} in (A \/ { {A}, { {A}}}) by XBOOLE_0:def 3;

        then

        reconsider W = {A}, V = { {A}} as Element of FS by A65, A66;

        

         A68: ( ConsecutiveSet2 (A, {} )) = A & ( ConsecutiveDelta2 (q, {} )) = D by Th14, Th18;

        ( ConsecutiveDelta2 (q,( succ {} ))) = ( new_bi_fun2 (( BiFun (( ConsecutiveDelta2 (q, {} )),( ConsecutiveSet2 (A, {} )),L)),( Quadr2 (q, {} )))) by Th19

        .= ( new_bi_fun2 (D,Q)) by A68, LATTICE5:def 15;

        then ( new_bi_fun2 (D,Q)) c= ( NextDelta2 q) by Th1, Th24;

        then

         A69: ( new_bi_fun2 (D,Q)) c= FD by A60;

        ( dom ( new_bi_fun2 (D,Q))) = [:( new_set2 A), ( new_set2 A):] & {A} in ( new_set2 A) by A67, FUNCT_2:def 1, XBOOLE_0:def 3;

        then [ {A}, { {A}}] in ( dom ( new_bi_fun2 (D,Q))) by A62, ZFMISC_1: 87;

        

        then (FD . (W,V)) = (( new_bi_fun2 (D,Q)) . ( {A}, { {A}})) by A69, GRFUNC_1: 2

        .= (((D . ((Q `1_4 ),(Q `2_4 ))) "\/" (Q `3_4 )) "/\" (Q `4_4 )) by Def4;

        then (FD . (W,V)) <= b by A59, YELLOW_0: 23;

        then [ {A}, { {A}}] in e by A58;

        hence thesis by A48, RELAT_1:def 10;

      end;

       A70:

      now

        consider e be Equivalence_Relation of FS such that e in the carrier of ( Image f) and

         A71: e <> ( id FS) by A47;

        assume FS is trivial;

        then

        consider x be object such that

         A72: FS = {x} by ZFMISC_1: 131;

        

         A73: [: {x}, {x}:] = { [x, x]} & ( id {x}) = { [x, x]} by SYSREL: 13, ZFMISC_1: 29;

        ( field e) = {x} by A72, EQREL_1: 9;

        then ( id FS) c= e by A72, RELAT_2: 1;

        hence contradiction by A72, A71, A73;

      end;

      D is onto by LATTICE5: 40;

      then

       A74: ( 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;

        

         A75: ((S . 0 ) `1 ) in the set of all ((S . i) `1 ) where i be Element of NAT ;

        

         A76: ((S . 0 ) `2 ) in the set of all ((S . i) `2 ) where i be Element of NAT ;

        

         A77: (S . 0 ) = [A, D] by Def11;

        

         A78: D c= FD by A76, A77, ZFMISC_1: 74;

        assume w in A;

        then

        consider z be object such that

         A79: z in [:A, A:] and

         A80: (D . z) = w by A74, FUNCT_2: 11;

        take z;

        A c= FS by A75, A77, ZFMISC_1: 74;

        then [:A, A:] c= [:FS, FS:] by ZFMISC_1: 96;

        hence z in [:FS, FS:] by A79;

        z in ( dom D) by A79, FUNCT_2:def 1;

        hence thesis by A80, A78, GRFUNC_1: 2;

      end;

      then ( rng FD) = A by FUNCT_2: 10;

      then

       A81: FD is onto by FUNCT_2:def 3;

      reconsider FS as non trivial set by A70;

      take FS;

      reconsider f as Homomorphism of L, ( EqRelLATT FS);

      take f;

      thus f is one-to-one by A81, LATTICE5: 15;

      reconsider FD as distance_function of FS, L;

      thus ( Image f) is finitely_typed

      proof

        take FS;

        thus for e be object st e in the carrier of ( Image f) holds e is Equivalence_Relation of FS

        proof

          let e be object;

          assume e in the carrier of ( Image f);

          then e in ( rng f) by YELLOW_0:def 15;

          then

          consider x be object such that

           A82: x in ( dom f) and

           A83: e = (f . x) by FUNCT_1:def 3;

          reconsider x as Element of L by A82;

          ex E be Equivalence_Relation of FS st E = (f . x) & for u,v be Element of FS holds [u, v] in E iff (FD . (u,v)) <= x by LATTICE5:def 8;

          hence thesis by A83;

        end;

        take (2 + 2);

        thus thesis by Th34;

      end;

      thus ex e be Equivalence_Relation of FS st e in the carrier of ( Image f) & e <> ( id FS)

      proof

        

         A84: {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

         A85: (Aq9,dq9) is_extension2_of (A9,d9) and

         A86: (S . 0 ) = [A9, d9] and

         A87: (S . ( 0 + 1)) = [Aq9, dq9] by Def11;

        A9 = A & d9 = D by A2, A86, XTUPLE_0: 1;

        then

        consider q be QuadrSeq of D such that

         A88: Aq9 = ( NextSet2 D) and

         A89: dq9 = ( NextDelta2 q) by A85;

        ( ConsecutiveSet2 (A, {} )) = A by Th14;

        then

        reconsider Q = ( Quadr2 (q, {} )) as Element of [:A, A, the carrier of L, the carrier of L:];

        

         A90: ((S . 1) `2 ) in the set of all ((S . i) `2 ) where i be Element of NAT ;

        ( succ {} ) c= ( DistEsti D) by Th1;

        then {} in ( DistEsti D) by ORDINAL1: 21;

        then

         A91: {} in ( dom q) by LATTICE5: 25;

        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 LATTICE5:def 13;

        then

        consider u,v be Element of A, a,b be Element of L such that

         A92: (q . {} ) = [u, v, a, b] and (D . (u,v)) <= (a "\/" b);

        consider e be Equivalence_Relation of FS such that

         A93: e = (f . b) and

         A94: for x,y be Element of FS holds [x, y] in e iff (FD . (x,y)) <= b by LATTICE5:def 8;

        ( Quadr2 (q, {} )) = [u, v, a, b] by A91, A92, Def6;

        then

         A95: b = (Q `4_4 );

        ( [Aq9, dq9] `2 ) = ( NextDelta2 q) by A89;

        then

         A96: ( NextDelta2 q) c= FD by A90, A87, ZFMISC_1: 74;

        

         A97: { {A}} in { {A}, { {A}}} by TARSKI:def 2;

        then

         A98: { {A}} in (A \/ { {A}, { {A}}}) by XBOOLE_0:def 3;

        take e;

        e in ( rng f) by A46, A93, FUNCT_1:def 3;

        hence e in the carrier of ( Image f) by YELLOW_0:def 15;

        

         A99: ((S . 1) `1 ) in the set of all ((S . i) `1 ) where i be Element of NAT ;

        ( [Aq9, dq9] `1 ) = ( NextSet2 D) by A88;

        then

         A100: ( NextSet2 D) c= FS by A99, A87, ZFMISC_1: 74;

        ( new_set2 A) = ( new_set2 ( ConsecutiveSet2 (A, {} ))) by Th14

        .= ( ConsecutiveSet2 (A,( succ {} ))) by Th15;

        then ( new_set2 A) c= ( NextSet2 D) by Th1, Th21;

        then

         A101: ( new_set2 A) c= FS by A100;

        

         A102: { {A}} in ( new_set2 A) by A97, XBOOLE_0:def 3;

        

         A103: {A} in { {A}, { {A}}} by TARSKI:def 2;

        then {A} in (A \/ { {A}, { {A}}}) by XBOOLE_0:def 3;

        then

        reconsider W = {A}, V = { {A}} as Element of FS by A101, A102;

        

         A104: ( ConsecutiveSet2 (A, {} )) = A & ( ConsecutiveDelta2 (q, {} )) = D by Th14, Th18;

        ( ConsecutiveDelta2 (q,( succ {} ))) = ( new_bi_fun2 (( BiFun (( ConsecutiveDelta2 (q, {} )),( ConsecutiveSet2 (A, {} )),L)),( Quadr2 (q, {} )))) by Th19

        .= ( new_bi_fun2 (D,Q)) by A104, LATTICE5:def 15;

        then ( new_bi_fun2 (D,Q)) c= ( NextDelta2 q) by Th1, Th24;

        then

         A105: ( new_bi_fun2 (D,Q)) c= FD by A96;

        ( dom ( new_bi_fun2 (D,Q))) = [:( new_set2 A), ( new_set2 A):] & {A} in ( new_set2 A) by A103, FUNCT_2:def 1, XBOOLE_0:def 3;

        then [ {A}, { {A}}] in ( dom ( new_bi_fun2 (D,Q))) by A98, ZFMISC_1: 87;

        

        then (FD . (W,V)) = (( new_bi_fun2 (D,Q)) . ( {A}, { {A}})) by A105, GRFUNC_1: 2

        .= (((D . ((Q `1_4 ),(Q `2_4 ))) "\/" (Q `3_4 )) "/\" (Q `4_4 )) by Def4;

        then (FD . (W,V)) <= b by A95, YELLOW_0: 23;

        then [ {A}, { {A}}] in e by A94;

        hence thesis by A84, RELAT_1:def 10;

      end;

      for e1,e2 be Equivalence_Relation of FS holds for 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) = (2 + 2) & (x,y) are_joint_by (F,e1,e2) by Th34;

      hence thesis by A47, LATTICE5: 13;

    end;

    ::$Notion-Name

    theorem :: LATTICE8:36

    for L be lower-bounded LATTICE holds L has_a_representation_of_type<= 2 iff L is modular by Th9, Th35;