lattice3.miz



    begin

    deffunc carr( LattStr) = the carrier of $1;

    deffunc join( LattStr) = the L_join of $1;

    deffunc met( LattStr) = the L_meet of $1;

    definition

      let X be set;

      :: LATTICE3:def1

      func BooleLatt X -> strict LattStr means

      : Def1: the carrier of it = ( bool X) & for Y,Z be Subset of X holds (the L_join of it . (Y,Z)) = (Y \/ Z) & (the L_meet of it . (Y,Z)) = (Y /\ Z);

      existence

      proof

        deffunc U( Subset of X, Subset of X) = ($1 \/ $2);

        consider j be BinOp of ( bool X) such that

         A1: for x,y be Subset of X holds (j . (x,y)) = U(x,y) from BINOP_1:sch 4;

        deffunc U( Subset of X, Subset of X) = ($1 /\ $2);

        consider m be BinOp of ( bool X) such that

         A2: for x,y be Subset of X holds (m . (x,y)) = U(x,y) from BINOP_1:sch 4;

        take LattStr (# ( bool X), j, m #);

        thus thesis by A1, A2;

      end;

      uniqueness

      proof

        let L1,L2 be strict LattStr such that

         A3: the carrier of L1 = ( bool X) and

         A4: for Y,Z be Subset of X holds ( join(L1) . (Y,Z)) = (Y \/ Z) & ( met(L1) . (Y,Z)) = (Y /\ Z) and

         A5: the carrier of L2 = ( bool X) and

         A6: for Y,Z be Subset of X holds ( join(L2) . (Y,Z)) = (Y \/ Z) & ( met(L2) . (Y,Z)) = (Y /\ Z);

        reconsider j1 = join(L1), j2 = join(L2), m1 = met(L1), m2 = met(L2) as BinOp of ( bool X) by A3, A5;

        now

          let x,y be Subset of X;

          

          thus (j1 . (x,y)) = (x \/ y) by A4

          .= (j2 . (x,y)) by A6;

        end;

        then

         A7: j1 = j2 by BINOP_1: 2;

        now

          let x,y be Subset of X;

          

          thus (m1 . (x,y)) = (x /\ y) by A4

          .= (m2 . (x,y)) by A6;

        end;

        hence thesis by A3, A5, A7, BINOP_1: 2;

      end;

    end

    reserve X for set,

x,y,z for Element of ( BooleLatt X),

s for set;

    registration

      let X be set;

      cluster ( BooleLatt X) -> non empty;

      coherence

      proof

        the carrier of ( BooleLatt X) = ( bool X) by Def1;

        hence the carrier of ( BooleLatt X) is non empty;

      end;

    end

    registration

      let X;

      let x, y;

      let x9,y9 be set;

      identify x9 \/ y9 with x "\/" y when x = x9, y = y9;

      compatibility

      proof

        reconsider x99 = x, y99 = y as Subset of X by Def1;

        assume that

         A1: x = x9 and

         A2: y = y9;

        

        thus (x "\/" y) = ( join(BooleLatt) . (x99,y99))

        .= (x9 \/ y9) by A1, A2, Def1;

      end;

      identify x9 /\ y9 with x "/\" y when x = x9, y = y9;

      compatibility

      proof

        reconsider x99 = x, y99 = y as Subset of X by Def1;

        assume that

         A3: x = x9 and

         A4: y = y9;

        

        thus (x "/\" y) = ( met(BooleLatt) . (x99,y99))

        .= (x9 /\ y9) by A3, A4, Def1;

      end;

    end

    theorem :: LATTICE3:1

    

     Th1: (x "\/" y) = (x \/ y) & (x "/\" y) = (x /\ y);

    theorem :: LATTICE3:2

    

     Th2: x [= y iff x c= y by XBOOLE_1: 7, XBOOLE_1: 12;

    registration

      let X;

      cluster ( BooleLatt X) -> Lattice-like;

      coherence

      proof

        

         A1: (x "\/" (y "\/" z)) = ((x "\/" y) "\/" z) by XBOOLE_1: 4;

        

         A2: ((x "/\" y) "\/" y) = y by XBOOLE_1: 22;

        

         A3: (x "/\" (y "/\" z)) = ((x "/\" y) "/\" z) by XBOOLE_1: 16;

        (x "/\" (x "\/" y)) = x by XBOOLE_1: 21;

        then ( BooleLatt X) is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing by A1, A2, A3;

        hence thesis;

      end;

    end

    reserve y for Element of ( BooleLatt X);

    theorem :: LATTICE3:3

    

     Th3: ( BooleLatt X) is lower-bounded & ( Bottom ( BooleLatt X)) = {}

    proof

       {} c= X;

      then

      reconsider x = {} as Element of ( BooleLatt X) by Def1;

      

       A1: (x "/\" y) = x;

      

       A2: (y "/\" x) = x;

      thus ( BooleLatt X) is lower-bounded

      proof

        take x;

        thus thesis;

      end;

      hence thesis by A1, A2, LATTICES:def 16;

    end;

    theorem :: LATTICE3:4

    

     Th4: ( BooleLatt X) is upper-bounded & ( Top ( BooleLatt X)) = X

    proof

      

       A1: ( bool X) = carr(BooleLatt) by Def1;

      then

      reconsider x = X as Element of ( BooleLatt X) by ZFMISC_1:def 1;

      

       A2: (x "\/" y) = x by A1, XBOOLE_1: 12;

      

       A3: (y "\/" x) = x by A1, XBOOLE_1: 12;

      thus ( BooleLatt X) is upper-bounded

      proof

        take x;

        thus thesis by A1, XBOOLE_1: 12;

      end;

      hence thesis by A2, A3, LATTICES:def 17;

    end;

    registration

      let X;

      cluster ( BooleLatt X) -> Boolean;

      coherence

      proof

        set B = ( BooleLatt X);

        

         A1: B is 0_Lattice by Th3;

        B is 1_Lattice by Th4;

        then

        reconsider B as 01_Lattice by A1;

        

         A2: B is complemented

        proof

          let x be Element of B;

          

           A3: carr(B) = ( bool X) by Def1;

          reconsider y = (X \ x) as Element of B by Def1;

          take y;

          

          thus (y "\/" x) = (y \/ x) by Th1

          .= (X \/ x) by XBOOLE_1: 39

          .= X by A3, XBOOLE_1: 12

          .= ( Top B) by Th4;

          hence (x "\/" y) = ( Top B);

          

           A4: y misses x by XBOOLE_1: 79;

          

          thus (y "/\" x) = (y /\ x) by Th1

          .= {} by A4

          .= ( Bottom B) by Th3;

          hence thesis;

        end;

        B is distributive

        proof

          let x,y,z be Element of B;

          

          thus (x "/\" (y "\/" z)) = (x /\ (y "\/" z)) by Th1

          .= (x /\ (y \/ z)) by Th1

          .= ((x /\ y) \/ (x /\ z)) by XBOOLE_1: 23

          .= ((x "/\" y) \/ (x /\ z)) by Th1

          .= ((x "/\" y) \/ (x "/\" z)) by Th1

          .= ((x "/\" y) "\/" (x "/\" z)) by Th1;

        end;

        hence thesis by A2;

      end;

    end

    theorem :: LATTICE3:5

    for x be Element of ( BooleLatt X) holds (x ` ) = (X \ x)

    proof

      set B = ( BooleLatt X);

      let x be Element of B;

      

       A1: ((x ` ) "/\" x) = ( Bottom B) by LATTICES: 20;

      

       A2: (x "\/" (x ` )) = ( Top B) by LATTICES: 21;

      

       A3: ( Bottom B) = {} by Th3;

      

       A4: ( Top B) = X by Th4;

      

       A5: (x ` ) misses x by A1, A3;

      

       A6: (X \ x) = ((x \ x) \/ ((x ` ) \ x)) by A2, A4, XBOOLE_1: 42;

      (x \ x) = {} by XBOOLE_1: 37;

      hence thesis by A5, A6, XBOOLE_1: 83;

    end;

    begin

    definition

      let L be Lattice;

      :: original: LattRel

      redefine

      func LattRel L -> Order of the carrier of L ;

      coherence

      proof

        

         A1: ( LattRel L) = { [p, q] where p be Element of L, q be Element of L : p [= q } by FILTER_1:def 8;

        ( LattRel L) c= [: carr(L), carr(L):]

        proof

          let x,y be object;

          assume [x, y] in ( LattRel L);

          then ex p,q be Element of L st [x, y] = [p, q] & p [= q by A1;

          hence thesis by ZFMISC_1: 87;

        end;

        then

        reconsider R = ( LattRel L) as Relation of carr(L);

        

         A2: R is_reflexive_in carr(L) by FILTER_1: 31;

        

         A3: R is_antisymmetric_in carr(L)

        proof

          let x,y be object;

          assume that

           A4: x in carr(L) and

           A5: y in carr(L);

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

          assume that

           A6: [x, y] in R and

           A7: [y, x] in R;

          

           A8: x9 [= y9 by A6, FILTER_1: 31;

          y9 [= x9 by A7, FILTER_1: 31;

          hence thesis by A8, LATTICES: 8;

        end;

        

         A9: R is_transitive_in carr(L)

        proof

          let x,y,z be object;

          assume that

           A10: x in carr(L) and

           A11: y in carr(L) and

           A12: z in carr(L);

          reconsider x9 = x, y9 = y, z9 = z as Element of L by A10, A11, A12;

          assume that

           A13: [x, y] in R and

           A14: [y, z] in R;

          

           A15: x9 [= y9 by A13, FILTER_1: 31;

          y9 [= z9 by A14, FILTER_1: 31;

          then x9 [= z9 by A15, LATTICES: 7;

          hence thesis by FILTER_1: 31;

        end;

        

         A16: ( dom R) = carr(L) by A2, ORDERS_1: 13;

        ( field R) = carr(L) by A2, ORDERS_1: 13;

        hence thesis by A2, A3, A9, A16, PARTFUN1:def 2, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16;

      end;

    end

    definition

      let L be Lattice;

      :: LATTICE3:def2

      func LattPOSet L -> strict Poset equals RelStr (# the carrier of L, ( LattRel L) #);

      correctness ;

    end

    registration

      let L be Lattice;

      cluster ( LattPOSet L) -> non empty;

      coherence ;

    end

    theorem :: LATTICE3:6

    

     Th6: for L1,L2 be Lattice st ( LattPOSet L1) = ( LattPOSet L2) holds the LattStr of L1 = the LattStr of L2

    proof

      let L1,L2 be Lattice such that

       A1: ( LattPOSet L1) = ( LattPOSet L2);

      reconsider j = join(L2), m = met(L2) as BinOp of carr(L1) by A1;

      now

        let a,b be Element of L1;

        reconsider x = a, y = b, xy = (a "\/" b) as Element of L2 by A1;

        reconsider ab = (x "\/" y) as Element of L1 by A1;

        

         A2: a [= (a "\/" b) by LATTICES: 5;

        

         A3: b [= (b "\/" a) by LATTICES: 5;

        

         A4: x [= (x "\/" y) by LATTICES: 5;

        

         A5: y [= (y "\/" x) by LATTICES: 5;

        

         A6: [x, xy] in ( LattRel L2) by A1, A2, FILTER_1: 31;

        

         A7: [y, xy] in ( LattRel L2) by A1, A3, FILTER_1: 31;

        

         A8: [a, ab] in ( LattRel L1) by A1, A4, FILTER_1: 31;

        

         A9: [b, ab] in ( LattRel L1) by A1, A5, FILTER_1: 31;

        

         A10: a [= ab by A8, FILTER_1: 31;

        

         A11: b [= ab by A9, FILTER_1: 31;

        

         A12: x [= xy by A6, FILTER_1: 31;

        

         A13: y [= xy by A7, FILTER_1: 31;

        

         A14: (a "\/" b) [= ab by A10, A11, FILTER_0: 6;

        (x "\/" y) [= xy by A12, A13, FILTER_0: 6;

        then [ab, (a "\/" b)] in ( LattRel L1) by A1, FILTER_1: 31;

        then ab [= (a "\/" b) by FILTER_1: 31;

        hence ( join(L1) . (a,b)) = (j . (a,b)) by A14, LATTICES: 8;

      end;

      then

       A15: join(L1) = j by BINOP_1: 2;

      now

        let a,b be Element of L1;

        reconsider x = a, y = b, xy = (a "/\" b) as Element of L2 by A1;

        reconsider ab = (x "/\" y) as Element of L1 by A1;

        

         A16: (a "/\" b) [= a by LATTICES: 6;

        

         A17: (b "/\" a) [= b by LATTICES: 6;

        

         A18: (x "/\" y) [= x by LATTICES: 6;

        

         A19: (y "/\" x) [= y by LATTICES: 6;

        

         A20: [xy, x] in ( LattRel L2) by A1, A16, FILTER_1: 31;

        

         A21: [xy, y] in ( LattRel L2) by A1, A17, FILTER_1: 31;

        

         A22: [ab, a] in ( LattRel L1) by A1, A18, FILTER_1: 31;

        

         A23: [ab, b] in ( LattRel L1) by A1, A19, FILTER_1: 31;

        

         A24: ab [= a by A22, FILTER_1: 31;

        

         A25: ab [= b by A23, FILTER_1: 31;

        

         A26: xy [= x by A20, FILTER_1: 31;

        

         A27: xy [= y by A21, FILTER_1: 31;

        

         A28: ab [= (a "/\" b) by A24, A25, FILTER_0: 7;

        xy [= (x "/\" y) by A26, A27, FILTER_0: 7;

        then [(a "/\" b), ab] in ( LattRel L1) by A1, FILTER_1: 31;

        then (a "/\" b) [= ab by FILTER_1: 31;

        hence ( met(L1) . (a,b)) = (m . (a,b)) by A28, LATTICES: 8;

      end;

      hence thesis by A1, A15, BINOP_1: 2;

    end;

    definition

      let L be Lattice, p be Element of L;

      :: LATTICE3:def3

      func p % -> Element of ( LattPOSet L) equals p;

      correctness ;

    end

    definition

      let L be Lattice, p be Element of ( LattPOSet L);

      :: LATTICE3:def4

      func % p -> Element of L equals p;

      correctness ;

    end

    reserve L for Lattice,

p,q for Element of L;

    theorem :: LATTICE3:7

    

     Th7: p [= q iff (p % ) <= (q % ) by FILTER_1: 31;

    definition

      let X be set, O be Order of X;

      :: original: ~

      redefine

      func O ~ -> Order of X ;

      coherence

      proof

        

         A1: ( dom O) = ( dom (O ~ )) by RELAT_2: 12;

        ( dom O) = X by PARTFUN1:def 2;

        hence thesis by A1, PARTFUN1:def 2;

      end;

    end

    definition

      let A be RelStr;

      :: LATTICE3:def5

      func A ~ -> strict RelStr equals RelStr (# the carrier of A, (the InternalRel of A ~ ) #);

      correctness ;

    end

    registration

      let A be Poset;

      cluster (A ~ ) -> reflexive transitive antisymmetric;

      coherence

      proof

        (A ~ ) = RelStr (# the carrier of A, (the InternalRel of A ~ ) #);

        hence thesis;

      end;

    end

    registration

      let A be non empty RelStr;

      cluster (A ~ ) -> non empty;

      coherence ;

    end

    reserve A for RelStr,

a,b,c for Element of A;

    theorem :: LATTICE3:8

    ((A ~ ) ~ ) = the RelStr of A;

    definition

      let A be RelStr, a be Element of A;

      :: LATTICE3:def6

      func a ~ -> Element of (A ~ ) equals a;

      correctness ;

    end

    definition

      let A be RelStr, a be Element of (A ~ );

      :: LATTICE3:def7

      func ~ a -> Element of A equals a;

      correctness ;

    end

    theorem :: LATTICE3:9

    

     Th9: a <= b iff (b ~ ) <= (a ~ ) by RELAT_1:def 7;

    definition

      let A be RelStr, X be set, a be Element of A;

      :: LATTICE3:def8

      pred a is_<=_than X means for b be Element of A st b in X holds a <= b;

      :: LATTICE3:def9

      pred X is_<=_than a means for b be Element of A st b in X holds b <= a;

    end

    notation

      let A be RelStr, X be set, a be Element of A;

      synonym X is_>=_than a for a is_<=_than X;

      synonym a is_>=_than X for X is_<=_than a;

    end

    definition

      let IT be RelStr;

      :: LATTICE3:def10

      attr IT is with_suprema means

      : Def10: for x,y be Element of IT holds ex z be Element of IT st x <= z & y <= z & for z9 be Element of IT st x <= z9 & y <= z9 holds z <= z9;

      :: LATTICE3:def11

      attr IT is with_infima means

      : Def11: for x,y be Element of IT holds ex z be Element of IT st z <= x & z <= y & for z9 be Element of IT st z9 <= x & z9 <= y holds z9 <= z;

    end

    registration

      cluster with_suprema -> non empty for RelStr;

      coherence

      proof

        let A be RelStr such that

         A1: for x,y be Element of A holds ex z be Element of A st x <= z & y <= z & for z9 be Element of A st x <= z9 & y <= z9 holds z <= z9;

        set x = the Element of A;

        consider z be Element of A such that

         A2: x <= z and x <= z and for z9 be Element of A st x <= z9 & x <= z9 holds z <= z9 by A1;

         [x, z] in the InternalRel of A by A2;

        hence thesis;

      end;

      cluster with_infima -> non empty for RelStr;

      coherence

      proof

        let A be RelStr such that

         A3: for x,y be Element of A holds ex z be Element of A st x >= z & y >= z & for z9 be Element of A st x >= z9 & y >= z9 holds z >= z9;

        set x = the Element of A;

        consider z be Element of A such that

         A4: x >= z and x >= z and for z9 be Element of A st x >= z9 & x >= z9 holds z >= z9 by A3;

         [z, x] in the InternalRel of A by A4;

        hence thesis;

      end;

    end

    theorem :: LATTICE3:10

    A is with_suprema iff (A ~ ) is with_infima

    proof

      thus A is with_suprema implies (A ~ ) is with_infima

      proof

        assume

         A1: for a, b holds ex c st a <= c & b <= c & for c9 be Element of A st a <= c9 & b <= c9 holds c <= c9;

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

        consider c such that

         A2: ( ~ x) <= c and

         A3: ( ~ y) <= c and

         A4: for c9 be Element of A st ( ~ x) <= c9 & ( ~ y) <= c9 holds c <= c9 by A1;

        take z = (c ~ );

        

         A5: (( ~ x) ~ ) = ( ~ x);

        

         A6: (( ~ y) ~ ) = ( ~ y);

        hence z <= x & z <= y by A2, A3, A5, Th9;

        let z9 be Element of (A ~ );

        

         A7: (( ~ z9) ~ ) = ( ~ z9);

        assume that

         A8: z9 <= x and

         A9: z9 <= y;

        

         A10: ( ~ x) <= ( ~ z9) by A5, A7, A8, Th9;

        ( ~ y) <= ( ~ z9) by A6, A7, A9, Th9;

        then c <= ( ~ z9) by A4, A10;

        hence thesis by A7, Th9;

      end;

      assume

       A11: for x,y be Element of (A ~ ) holds ex z be Element of (A ~ ) st z <= x & z <= y & for z9 be Element of (A ~ ) st z9 <= x & z9 <= y holds z9 <= z;

      let a, b;

      consider z be Element of (A ~ ) such that

       A12: z <= (a ~ ) and

       A13: z <= (b ~ ) and

       A14: for z9 be Element of (A ~ ) st z9 <= (a ~ ) & z9 <= (b ~ ) holds z9 <= z by A11;

      take c = ( ~ z);

      

       A15: (( ~ z) ~ ) = ( ~ z);

      hence a <= c & b <= c by A12, A13, Th9;

      let c9 be Element of A;

      assume that

       A16: a <= c9 and

       A17: b <= c9;

      

       A18: (c9 ~ ) <= (a ~ ) by A16, Th9;

      (c9 ~ ) <= (b ~ ) by A17, Th9;

      then (c9 ~ ) <= z by A14, A18;

      hence thesis by A15, Th9;

    end;

    theorem :: LATTICE3:11

    for L be Lattice holds ( LattPOSet L) is with_suprema with_infima

    proof

      let L;

      thus ( LattPOSet L) is with_suprema

      proof

        let x,y be Element of ( LattPOSet L);

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

        

         A1: ( % x) [= (( % x) "\/" ( % y)) by LATTICES: 5;

        

         A2: ( % y) [= (( % y) "\/" ( % x)) by LATTICES: 5;

        

         A3: (( % x) % ) = ( % x);

        

         A4: (( % y) % ) = ( % y);

        hence x <= z & y <= z by A1, A2, A3, Th7;

        let z9 be Element of ( LattPOSet L);

        

         A5: (( % z9) % ) = ( % z9);

        assume that

         A6: x <= z9 and

         A7: y <= z9;

        

         A8: ( % x) [= ( % z9) by A3, A5, A6, Th7;

        ( % y) [= ( % z9) by A4, A5, A7, Th7;

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

        hence thesis by A5, Th7;

      end;

      let x,y be Element of ( LattPOSet L);

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

      

       A9: (( % x) "/\" ( % y)) [= ( % x) by LATTICES: 6;

      

       A10: (( % y) "/\" ( % x)) [= ( % y) by LATTICES: 6;

      

       A11: (( % x) % ) = ( % x);

      

       A12: (( % y) % ) = ( % y);

      hence z <= x & z <= y by A9, A10, A11, Th7;

      let z9 be Element of ( LattPOSet L);

      

       A13: (( % z9) % ) = ( % z9);

      assume that

       A14: z9 <= x and

       A15: z9 <= y;

      

       A16: ( % z9) [= ( % x) by A11, A13, A14, Th7;

      ( % z9) [= ( % y) by A12, A13, A15, Th7;

      then ( % z9) [= (( % x) "/\" ( % y)) by A16, FILTER_0: 7;

      hence thesis by A13, Th7;

    end;

    definition

      let IT be RelStr;

      :: LATTICE3:def12

      attr IT is complete means

      : Def12: for X be set holds ex a be Element of IT st X is_<=_than a & for b be Element of IT st X is_<=_than b holds a <= b;

    end

    registration

      cluster strict complete non empty for Poset;

      existence

      proof

        set s = the set;

        set D = {s};

        set R = the Order of D;

        take A = RelStr (# D, R #);

        thus A is strict;

        hereby

          let X be set;

          reconsider s as Element of A by TARSKI:def 1;

          take s;

          thus X is_<=_than s

          proof

            let a be Element of A such that a in X;

            thus a <= s by TARSKI:def 1;

          end;

          let b be Element of A such that X is_<=_than b;

          thus s <= b by TARSKI:def 1;

        end;

        thus thesis;

      end;

    end

    reserve A for non empty RelStr,

a,b,c,c9 for Element of A;

    theorem :: LATTICE3:12

    

     Th12: A is complete implies A is with_suprema with_infima

    proof

      assume

       A1: for X be set holds ex a st X is_<=_than a & for b st X is_<=_than b holds a <= b;

      thus A is with_suprema

      proof

        let a, b;

        consider c such that

         A2: {a, b} is_<=_than c and

         A3: for c9 st {a, b} is_<=_than c9 holds c <= c9 by A1;

        take c;

        

         A4: a in {a, b} by TARSKI:def 2;

        b in {a, b} by TARSKI:def 2;

        hence a <= c & b <= c by A2, A4;

        let c9 such that

         A5: a <= c9 and

         A6: b <= c9;

         {a, b} is_<=_than c9 by A5, A6, TARSKI:def 2;

        hence thesis by A3;

      end;

      let a, b;

      set X = { c : c <= a & c <= b };

      consider c such that

       A7: X is_<=_than c and

       A8: for c9 st X is_<=_than c9 holds c <= c9 by A1;

      take c;

      X is_<=_than a

      proof

        let c;

        assume c in X;

        then ex c9 st c = c9 & c9 <= a & c9 <= b;

        hence thesis;

      end;

      hence c <= a by A8;

      X is_<=_than b

      proof

        let c;

        assume c in X;

        then ex c9 st c = c9 & c9 <= a & c9 <= b;

        hence thesis;

      end;

      hence c <= b by A8;

      let c9;

      assume that

       A9: c9 <= a and

       A10: c9 <= b;

      c9 in X by A9, A10;

      hence thesis by A7;

    end;

    registration

      cluster complete with_suprema with_infima strict non empty for Poset;

      existence

      proof

        set A = the complete strict non empty Poset;

        take A;

        thus thesis by Th12;

      end;

    end

    definition

      let A be RelStr;

      let a,b be Element of A;

      :: LATTICE3:def13

      func a "\/" b -> Element of A means

      : Def13: a <= it & b <= it & for c be Element of A st a <= c & b <= c holds it <= c;

      existence by A2;

      uniqueness

      proof

        let c1,c2 be Element of A such that

         A3: a <= c1 and

         A4: b <= c1 and

         A5: for c be Element of A st a <= c & b <= c holds c1 <= c and

         A6: a <= c2 and

         A7: b <= c2 and

         A8: for c be Element of A st a <= c & b <= c holds c2 <= c;

        

         A9: c1 <= c2 by A5, A6, A7;

        c2 <= c1 by A3, A4, A8;

        hence thesis by A1, A9, ORDERS_2: 2;

      end;

    end

     Lm1:

    now

      let A be non empty antisymmetric with_suprema RelStr;

      let a,b be Element of A;

      ex x be Element of A st a <= x & b <= x & for c be Element of A st a <= c & b <= c holds x <= c by Def10;

      hence for c be Element of A holds c = (a "\/" b) iff a <= c & b <= c & for d be Element of A st a <= d & b <= d holds c <= d by Def13;

    end;

    definition

      let A be RelStr;

      let a,b be Element of A;

      :: LATTICE3:def14

      func a "/\" b -> Element of A means

      : Def14: it <= a & it <= b & for c be Element of A st c <= a & c <= b holds c <= it ;

      existence by A2;

      uniqueness

      proof

        let c1,c2 be Element of A such that

         A3: c1 <= a and

         A4: c1 <= b and

         A5: for c be Element of A st c <= a & c <= b holds c <= c1 and

         A6: c2 <= a and

         A7: c2 <= b and

         A8: for c be Element of A st c <= a & c <= b holds c <= c2;

        

         A9: c1 <= c2 by A3, A4, A8;

        c2 <= c1 by A5, A6, A7;

        hence thesis by A1, A9, ORDERS_2: 2;

      end;

    end

     Lm2:

    now

      let A be non empty antisymmetric with_infima RelStr;

      let a,b be Element of A;

      ex x be Element of A st a >= x & b >= x & for c be Element of A st a >= c & b >= c holds x >= c by Def11;

      hence for c be Element of A holds c = (a "/\" b) iff a >= c & b >= c & for d be Element of A st a >= d & b >= d holds c >= d by Def14;

    end;

    reserve V for with_suprema antisymmetric RelStr,

u1,u2,u3,u4 for Element of V;

    reserve N for with_infima antisymmetric RelStr,

n1,n2,n3,n4 for Element of N;

    reserve K for with_suprema with_infima reflexive antisymmetric RelStr,

k1,k2,k3 for Element of K;

    theorem :: LATTICE3:13

    

     Th13: (u1 "\/" u2) = (u2 "\/" u1)

    proof

      

       A1: u1 <= (u1 "\/" u2) by Lm1;

      

       A2: u2 <= (u1 "\/" u2) by Lm1;

      for u3 st u2 <= u3 & u1 <= u3 holds (u1 "\/" u2) <= u3 by Lm1;

      hence thesis by A1, A2, Def13;

    end;

    theorem :: LATTICE3:14

    

     Th14: V is transitive implies ((u1 "\/" u2) "\/" u3) = (u1 "\/" (u2 "\/" u3))

    proof

      assume

       A1: V is transitive;

      

       A2: u1 <= (u1 "\/" u2) by Lm1;

      

       A3: u2 <= (u1 "\/" u2) by Lm1;

      

       A4: u2 <= (u2 "\/" u3) by Lm1;

      

       A5: u3 <= (u2 "\/" u3) by Lm1;

      

       A6: (u1 "\/" u2) <= ((u1 "\/" u2) "\/" u3) by Lm1;

      

       A7: u3 <= ((u1 "\/" u2) "\/" u3) by Lm1;

      

       A8: u1 <= ((u1 "\/" u2) "\/" u3) by A1, A2, A6, ORDERS_2: 3;

      u2 <= ((u1 "\/" u2) "\/" u3) by A1, A3, A6, ORDERS_2: 3;

      then

       A9: (u2 "\/" u3) <= ((u1 "\/" u2) "\/" u3) by A7, Lm1;

      now

        let u4;

        assume that

         A10: u1 <= u4 and

         A11: (u2 "\/" u3) <= u4;

        

         A12: u2 <= u4 by A1, A4, A11, ORDERS_2: 3;

        

         A13: u3 <= u4 by A1, A5, A11, ORDERS_2: 3;

        (u1 "\/" u2) <= u4 by A10, A12, Lm1;

        hence ((u1 "\/" u2) "\/" u3) <= u4 by A13, Lm1;

      end;

      hence thesis by A8, A9, Def13;

    end;

    theorem :: LATTICE3:15

    

     Th15: (n1 "/\" n2) = (n2 "/\" n1)

    proof

      

       A1: (n1 "/\" n2) <= n1 by Lm2;

      

       A2: (n1 "/\" n2) <= n2 by Lm2;

      for n3 st n3 <= n2 & n3 <= n1 holds n3 <= (n1 "/\" n2) by Lm2;

      hence thesis by A1, A2, Def14;

    end;

    theorem :: LATTICE3:16

    

     Th16: N is transitive implies ((n1 "/\" n2) "/\" n3) = (n1 "/\" (n2 "/\" n3))

    proof

      assume

       A1: N is transitive;

      

       A2: (n1 "/\" n2) <= n1 by Lm2;

      

       A3: (n1 "/\" n2) <= n2 by Lm2;

      

       A4: (n2 "/\" n3) <= n2 by Lm2;

      

       A5: (n2 "/\" n3) <= n3 by Lm2;

      

       A6: ((n1 "/\" n2) "/\" n3) <= (n1 "/\" n2) by Lm2;

      

       A7: ((n1 "/\" n2) "/\" n3) <= n3 by Lm2;

      

       A8: ((n1 "/\" n2) "/\" n3) <= n1 by A1, A2, A6, ORDERS_2: 3;

      ((n1 "/\" n2) "/\" n3) <= n2 by A1, A3, A6, ORDERS_2: 3;

      then

       A9: ((n1 "/\" n2) "/\" n3) <= (n2 "/\" n3) by A7, Lm2;

      now

        let n4;

        assume that

         A10: n4 <= n1 and

         A11: n4 <= (n2 "/\" n3);

        

         A12: n4 <= n2 by A1, A4, A11, ORDERS_2: 3;

        

         A13: n4 <= n3 by A1, A5, A11, ORDERS_2: 3;

        n4 <= (n1 "/\" n2) by A10, A12, Lm2;

        hence n4 <= ((n1 "/\" n2) "/\" n3) by A13, Lm2;

      end;

      hence thesis by A8, A9, Def14;

    end;

    definition

      let L be with_infima antisymmetric RelStr, x,y be Element of L;

      :: original: "/\"

      redefine

      func x "/\" y;

      commutativity by Th15;

    end

    definition

      let L be with_suprema antisymmetric RelStr, x,y be Element of L;

      :: original: "\/"

      redefine

      func x "\/" y;

      commutativity by Th13;

    end

    theorem :: LATTICE3:17

    

     Th17: ((k1 "/\" k2) "\/" k2) = k2

    proof

      

       A1: (k1 "/\" k2) <= k2 by Lm2;

      

       A2: k2 <= k2;

      for k3 st (k1 "/\" k2) <= k3 & k2 <= k3 holds k2 <= k3;

      hence thesis by A1, A2, Def13;

    end;

    theorem :: LATTICE3:18

    

     Th18: (k1 "/\" (k1 "\/" k2)) = k1

    proof

      

       A1: k1 <= k1;

      

       A2: k1 <= (k1 "\/" k2) by Lm1;

      for k3 st k3 <= k1 & k3 <= (k1 "\/" k2) holds k3 <= k1;

      hence thesis by A1, A2, Def14;

    end;

    theorem :: LATTICE3:19

    

     Th19: for A be with_suprema with_infima Poset holds ex L be strict Lattice st the RelStr of A = ( LattPOSet L)

    proof

      let A be with_suprema with_infima Poset;

      defpred X[ Element of A, Element of A, set] means for x9,y9 be Element of A st x9 = $1 & y9 = $2 holds $3 = (x9 "\/" y9);

      

       A1: for x,y be Element of A holds ex u be Element of A st X[x, y, u]

      proof

        let x,y be Element of A;

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

        take (x9 "\/" y9);

        thus thesis;

      end;

      consider j be BinOp of the carrier of A such that

       A2: for x,y be Element of A holds X[x, y, (j . (x,y))] from BINOP_1:sch 3( A1);

      defpred X[ Element of A, Element of A, set] means for x9,y9 be Element of A st x9 = $1 & y9 = $2 holds $3 = (x9 "/\" y9);

      

       A3: for x,y be Element of A holds ex u be Element of A st X[x, y, u]

      proof

        let x,y be Element of A;

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

        take (x9 "/\" y9);

        thus thesis;

      end;

      consider m be BinOp of the carrier of A such that

       A4: for x,y be Element of A holds X[x, y, (m . (x,y))] from BINOP_1:sch 3( A3);

      set L = LattStr (# the carrier of A, j, m #);

       A5:

      now

        let a,b be Element of L;

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

        (j . (x,y)) = (x "\/" y) by A2;

        hence (a "\/" b) = (b "\/" a) by A2;

      end;

       A6:

      now

        let a,b,c be Element of L;

        reconsider x = a, y = b, z = c as Element of A;

        

        thus (a "\/" (b "\/" c)) = (j . (x,(y "\/" z))) by A2

        .= (x "\/" (y "\/" z)) by A2

        .= ((x "\/" y) "\/" z) by Th14

        .= (j . ((x "\/" y),z)) by A2

        .= ((a "\/" b) "\/" c) by A2;

      end;

       A7:

      now

        let a,b be Element of L;

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

        

        thus ((a "/\" b) "\/" b) = (j . ((x "/\" y),y)) by A4

        .= ((x "/\" y) "\/" y) by A2

        .= b by Th17;

      end;

       A8:

      now

        let a,b be Element of L;

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

        (m . (x,y)) = (x "/\" y) by A4;

        hence (a "/\" b) = (b "/\" a) by A4;

      end;

       A9:

      now

        let a,b,c be Element of L;

        reconsider x = a, y = b, z = c as Element of A;

        

        thus (a "/\" (b "/\" c)) = (m . (x,(y "/\" z))) by A4

        .= (x "/\" (y "/\" z)) by A4

        .= ((x "/\" y) "/\" z) by Th16

        .= (m . ((x "/\" y),z)) by A4

        .= ((a "/\" b) "/\" c) by A4;

      end;

      now

        let a,b be Element of L;

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

        

        thus (a "/\" (a "\/" b)) = (m . (x,(x "\/" y))) by A2

        .= (x "/\" (x "\/" y)) by A4

        .= a by Th18;

      end;

      then L is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing by A5, A6, A7, A8, A9;

      then

      reconsider L as strict Lattice;

      take L;

      

       A10: ( LattRel L) = { [p, q] where p be Element of L, q be Element of L : p [= q } by FILTER_1:def 8;

      ( LattRel L) = the InternalRel of A

      proof

        let x,y be object;

        thus [x, y] in ( LattRel L) implies [x, y] in the InternalRel of A

        proof

          assume [x, y] in ( LattRel L);

          then

          consider p,q be Element of L such that

           A11: [x, y] = [p, q] and

           A12: p [= q by A10;

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

          (p9 "\/" q9) = (p "\/" q) by A2

          .= q by A12;

          then p9 <= q9 by Lm1;

          hence thesis by A11;

        end;

        assume

         A13: [x, y] in the InternalRel of A;

        then

        consider x1,x2 be object such that

         A14: x1 in the carrier of A and

         A15: x2 in the carrier of A and

         A16: [x, y] = [x1, x2] by ZFMISC_1: 84;

        reconsider x1, x2 as Element of A by A14, A15;

        reconsider y1 = x1, y2 = x2 as Element of L;

        

         A17: x1 <= x2 by A13, A16;

        x2 <= x2;

        then

         A18: (x1 "\/" x2) <= x2 by A17, Lm1;

        x2 <= (x1 "\/" x2) by Lm1;

        

        then x2 = (x1 "\/" x2) by A18, ORDERS_2: 2

        .= (y1 "\/" y2) by A2;

        then y1 [= y2;

        hence thesis by A10, A16;

      end;

      hence thesis;

    end;

    definition

      let A be RelStr;

      :: LATTICE3:def15

      func latt A -> strict Lattice means

      : Def15: the RelStr of A = ( LattPOSet it );

      existence by A1, Th19;

      uniqueness by Th6;

    end

    theorem :: LATTICE3:20

    (( LattRel L) ~ ) = ( LattRel (L .: )) & (( LattPOSet L) ~ ) = ( LattPOSet (L .: ))

    proof

      

       A1: ( LattRel L) = { [p, q] : p [= q } by FILTER_1:def 8;

      

       A2: ( LattRel (L .: )) = { [p9, q9] where p9 be Element of (L .: ), q9 be Element of (L .: ) : p9 [= q9 } by FILTER_1:def 8;

      

       A3: (L .: ) = LattStr (# carr(L), met(L), join(L) #) by LATTICE2:def 2;

      thus (( LattRel L) ~ ) = ( LattRel (L .: ))

      proof

        let x,y be object;

        thus [x, y] in (( LattRel L) ~ ) implies [x, y] in ( LattRel (L .: ))

        proof

          assume [x, y] in (( LattRel L) ~ );

          then [y, x] in ( LattRel L) by RELAT_1:def 7;

          then

          consider p, q such that

           A4: [y, x] = [p, q] and

           A5: p [= q by A1;

          reconsider p9 = p, q9 = q as Element of (L .: ) by A3;

          

           A6: x = q by A4, XTUPLE_0: 1;

          

           A7: y = p by A4, XTUPLE_0: 1;

          q9 [= p9 by A5, LATTICE2: 38;

          hence thesis by A2, A6, A7;

        end;

        assume [x, y] in ( LattRel (L .: ));

        then

        consider p9,q9 be Element of (L .: ) such that

         A8: [x, y] = [p9, q9] and

         A9: p9 [= q9 by A2;

        reconsider p = p9, q = q9 as Element of L by A3;

        

         A10: x = p by A8, XTUPLE_0: 1;

        

         A11: y = q by A8, XTUPLE_0: 1;

        q [= p by A9, LATTICE2: 39;

        then [y, x] in ( LattRel L) by A1, A10, A11;

        hence thesis by RELAT_1:def 7;

      end;

      hence thesis by A3;

    end;

    begin

    definition

      let L be non empty LattStr, p be Element of L, X be set;

      :: LATTICE3:def16

      pred p is_less_than X means for q be Element of L st q in X holds p [= q;

      :: LATTICE3:def17

      pred X is_less_than p means for q be Element of L st q in X holds q [= p;

    end

    notation

      let L be non empty LattStr, p be Element of L, X be set;

      synonym X is_greater_than p for p is_less_than X;

      synonym p is_greater_than X for X is_less_than p;

    end

    theorem :: LATTICE3:21

    for L be Lattice, p,q,r be Element of L holds p is_less_than {q, r} iff p [= (q "/\" r)

    proof

      let L be Lattice, p,q,r be Element of L;

      

       A1: q in {q, r} by TARSKI:def 2;

      

       A2: r in {q, r} by TARSKI:def 2;

      thus p is_less_than {q, r} implies p [= (q "/\" r)

      proof

        assume

         A3: p is_less_than {q, r};

        then

         A4: p [= q by A1;

        p [= r by A2, A3;

        hence thesis by A4, FILTER_0: 7;

      end;

      assume

       A5: p [= (q "/\" r);

      let a be Element of L;

      assume a in {q, r};

      then

       A6: a = q or a = r by TARSKI:def 2;

      

       A7: (q "/\" r) [= q by LATTICES: 6;

      (r "/\" q) [= r by LATTICES: 6;

      hence thesis by A5, A6, A7, LATTICES: 7;

    end;

    theorem :: LATTICE3:22

    for L be Lattice, p,q,r be Element of L holds p is_greater_than {q, r} iff (q "\/" r) [= p

    proof

      let L be Lattice, p,q,r be Element of L;

      

       A1: q in {q, r} by TARSKI:def 2;

      

       A2: r in {q, r} by TARSKI:def 2;

      thus p is_greater_than {q, r} implies (q "\/" r) [= p

      proof

        assume

         A3: p is_greater_than {q, r};

        then

         A4: q [= p by A1;

        r [= p by A2, A3;

        hence thesis by A4, FILTER_0: 6;

      end;

      assume

       A5: (q "\/" r) [= p;

      let a be Element of L;

      assume a in {q, r};

      then

       A6: a = q or a = r by TARSKI:def 2;

      

       A7: q [= (q "\/" r) by LATTICES: 5;

      r [= (r "\/" q) by LATTICES: 5;

      hence thesis by A5, A6, A7, LATTICES: 7;

    end;

    definition

      let IT be non empty LattStr;

      :: LATTICE3:def18

      attr IT is complete means

      : Def18: for X be set holds ex p be Element of IT st X is_less_than p & for r be Element of IT st X is_less_than r holds p [= r;

      :: LATTICE3:def19

      attr IT is \/-distributive means for X holds for a,b,c be Element of IT st X is_less_than a & (for d be Element of IT st X is_less_than d holds a [= d) & { (b "/\" a9) where a9 be Element of IT : a9 in X } is_less_than c & for d be Element of IT st { (b "/\" a9) where a9 be Element of IT : a9 in X } is_less_than d holds c [= d holds (b "/\" a) [= c;

      :: LATTICE3:def20

      attr IT is /\-distributive means for X holds for a,b,c be Element of IT st X is_greater_than a & (for d be Element of IT st X is_greater_than d holds d [= a) & { (b "\/" a9) where a9 be Element of IT : a9 in X } is_greater_than c & for d be Element of IT st { (b "\/" a9) where a9 be Element of IT : a9 in X } is_greater_than d holds d [= c holds c [= (b "\/" a);

    end

    theorem :: LATTICE3:23

    for B be B_Lattice, a be Element of B holds X is_less_than a iff { (b ` ) where b be Element of B : b in X } is_greater_than (a ` )

    proof

      let B be B_Lattice, a be Element of B;

      set Y = { (b ` ) where b be Element of B : b in X };

      thus X is_less_than a implies Y is_greater_than (a ` )

      proof

        assume

         A1: for b be Element of B st b in X holds b [= a;

        let b be Element of B;

        assume b in Y;

        then ex c be Element of B st (b = (c ` )) & (c in X);

        hence thesis by A1, LATTICES: 26;

      end;

      assume

       A2: for b be Element of B st b in Y holds (a ` ) [= b;

      let b be Element of B;

      assume b in X;

      then

       A3: (b ` ) in Y;

      

       A4: ((a ` ) ` ) = a;

      ((b ` ) ` ) = b;

      hence thesis by A2, A3, A4, LATTICES: 26;

    end;

    theorem :: LATTICE3:24

    

     Th24: for B be B_Lattice, a be Element of B holds X is_greater_than a iff { (b ` ) where b be Element of B : b in X } is_less_than (a ` )

    proof

      let B be B_Lattice, a be Element of B;

      set Y = { (b ` ) where b be Element of B : b in X };

      thus X is_greater_than a implies Y is_less_than (a ` )

      proof

        assume

         A1: for b be Element of B st b in X holds a [= b;

        let b be Element of B;

        assume b in Y;

        then ex c be Element of B st (b = (c ` )) & (c in X);

        hence thesis by A1, LATTICES: 26;

      end;

      assume

       A2: for b be Element of B st b in Y holds b [= (a ` );

      let b be Element of B;

      assume b in X;

      then

       A3: (b ` ) in Y;

      

       A4: ((a ` ) ` ) = a;

      ((b ` ) ` ) = b;

      hence thesis by A2, A3, A4, LATTICES: 26;

    end;

    theorem :: LATTICE3:25

    

     Th25: ( BooleLatt X) is complete

    proof

      set B = ( BooleLatt X);

      let x be set;

      set p = ( union (x /\ ( bool X)));

      

       A1: carr(B) = ( bool X) by Def1;

      reconsider p as Element of B by Def1;

      take p;

      thus x is_less_than p

      proof

        let q be Element of B;

        assume q in x;

        then q in (x /\ ( bool X)) by A1, XBOOLE_0:def 4;

        then q c= p by ZFMISC_1: 74;

        hence thesis by Th2;

      end;

      let r be Element of B such that

       A2: for q be Element of B st q in x holds q [= r;

      now

        let z be set;

        assume

         A3: z in (x /\ ( bool X));

        then

         A4: z in x by XBOOLE_0:def 4;

        reconsider z9 = z as Element of B by A1, A3;

        z9 [= r by A2, A4;

        hence z c= r by Th2;

      end;

      then p c= r by ZFMISC_1: 76;

      hence thesis by Th2;

    end;

    registration

      let X be set;

      cluster ( BooleLatt X) -> complete;

      coherence by Th25;

    end

    theorem :: LATTICE3:26

    

     Th26: ( BooleLatt X) is \/-distributive

    proof

      let x be set;

      set B = ( BooleLatt X);

      let a,b,c be Element of B such that

       A1: x is_less_than a and

       A2: for d be Element of B st x is_less_than d holds a [= d and

       A3: { (b "/\" a9) where a9 be Element of B : a9 in x } is_less_than c and

       A4: for d be Element of B st { (b "/\" a9) where a9 be Element of B : a9 in x } is_less_than d holds c [= d;

      set Y = { (b "/\" a9) where a9 be Element of B : a9 in x };

      

       A5: carr(B) = ( bool X) by Def1;

      

       A6: Y c= ( bool X)

      proof

        let z be object;

        assume z in Y;

        then ex a9 be Element of B st z = (b "/\" a9) & a9 in x;

        hence thesis by A5;

      end;

      

       A7: ( union Y) c= ( union ( bool X)) by A6, ZFMISC_1: 77;

      ( union ( bool X)) = X by ZFMISC_1: 81;

      then

      reconsider p = ( union (x /\ ( bool X))), q = ( union Y) as Element of B by A7, Def1;

      now

        let y be set;

        assume

         A8: y in (x /\ ( bool X));

        then

         A9: y in x by XBOOLE_0:def 4;

        reconsider y9 = y as Element of B by A5, A8;

        y9 [= a by A1, A9;

        hence y c= a by Th2;

      end;

      then

       A10: p c= a by ZFMISC_1: 76;

      

       A11: x is_less_than p

      proof

        let q be Element of B;

        assume q in x;

        then q in (x /\ ( bool X)) by A5, XBOOLE_0:def 4;

        then q c= p by ZFMISC_1: 74;

        hence q [= p by Th2;

      end;

      

       A12: p [= a by A10, Th2;

      a [= p by A2, A11;

      then

       A13: a = p by A12;

      now

        let y be set;

        assume

         A14: y in Y;

        then

        consider a9 be Element of B such that

         A15: y = (b "/\" a9) and a9 in x;

        (b "/\" a9) [= c by A3, A14, A15;

        hence y c= c by A15, Th2;

      end;

      then

       A16: q c= c by ZFMISC_1: 76;

      

       A17: Y is_less_than q by ZFMISC_1: 74, Th2;

      

       A18: q [= c by A16, Th2;

      c [= q by A4, A17;

      then

       A19: c = q by A18;

      (b /\ a) c= c

      proof

        let z be object;

        assume

         A20: z in (b /\ a);

        then

         A21: z in b by XBOOLE_0:def 4;

        z in a by A20, XBOOLE_0:def 4;

        then

        consider y be set such that

         A22: z in y and

         A23: y in (x /\ ( bool X)) by A13, TARSKI:def 4;

        

         A24: y in x by A23, XBOOLE_0:def 4;

        reconsider y as Element of B by A5, A23;

        

         A25: (b "/\" y) in Y by A24;

        z in (b /\ y) by A21, A22, XBOOLE_0:def 4;

        hence thesis by A19, A25, TARSKI:def 4;

      end;

      hence (b "/\" a) [= c by Th2;

    end;

    theorem :: LATTICE3:27

    

     Th27: ( BooleLatt X) is /\-distributive

    proof

      let x be set;

      set B = ( BooleLatt X);

      let a,b,c be Element of B such that

       A1: x is_greater_than a and

       A2: for d be Element of B st x is_greater_than d holds d [= a and

       A3: { (b "\/" a9) where a9 be Element of B : a9 in x } is_greater_than c and

       A4: for d be Element of B st { (b "\/" a9) where a9 be Element of B : a9 in x } is_greater_than d holds d [= c;

      set x9 = { (e ` ) where e be Element of B : e in x }, y = { (b "\/" e) where e be Element of B : e in x }, y9 = { (e ` ) where e be Element of B : e in y }, z = { ((b ` ) "/\" e) where e be Element of B : e in x9 };

      

       A5: z = y9

      proof

        thus z c= y9

        proof

          let s be object;

          assume s in z;

          then

          consider e be Element of B such that

           A6: s = ((b ` ) "/\" e) and

           A7: e in x9;

          consider i be Element of B such that

           A8: e = (i ` ) and

           A9: i in x by A7;

          

           A10: (b "\/" i) in y by A9;

          ((b "\/" i) ` ) = s by A6, A8, LATTICES: 24;

          hence thesis by A10;

        end;

        let s be object;

        assume s in y9;

        then

        consider e be Element of B such that

         A11: s = (e ` ) and

         A12: e in y;

        consider i be Element of B such that

         A13: e = (b "\/" i) and

         A14: i in x by A12;

        

         A15: (i ` ) in x9 by A14;

        s = ((b ` ) "/\" (i ` )) by A11, A13, LATTICES: 24;

        hence thesis by A15;

      end;

      

       A16: ((c ` ) ` ) = c;

      

       A17: x9 is_less_than (a ` ) by A1, Th24;

      

       A18: for d be Element of B st x9 is_less_than d holds (a ` ) [= d

      proof

        let d be Element of B;

        

         A19: ((d ` ) ` ) = d;

        assume x9 is_less_than d;

        then x is_greater_than (d ` ) by A19, Th24;

        hence thesis by A2, A19, LATTICES: 26;

      end;

      

       A20: z is_less_than (c ` ) by A3, A5, Th24;

      

       A21: for d be Element of B st z is_less_than d holds (c ` ) [= d

      proof

        let d be Element of B;

        

         A22: ((d ` ) ` ) = d;

        assume z is_less_than d;

        then y is_greater_than (d ` ) by A5, A22, Th24;

        hence thesis by A4, A22, LATTICES: 26;

      end;

      B is \/-distributive by Th26;

      then

       A23: ((b ` ) "/\" (a ` )) [= (c ` ) by A17, A18, A20, A21;

      (((b ` ) "/\" (a ` )) ` ) = (((b ` ) ` ) "\/" ((a ` ) ` )) by LATTICES: 23;

      hence c [= (b "\/" a) by A16, A23, LATTICES: 26;

    end;

    registration

      cluster complete \/-distributive /\-distributive strict for Lattice;

      existence

      proof

        set X = the set;

        ( BooleLatt X) is complete \/-distributive /\-distributive by Th26, Th27;

        hence thesis;

      end;

    end

    reserve p9,q9 for Element of ( LattPOSet L);

    theorem :: LATTICE3:28

    

     Th28: p is_less_than X iff (p % ) is_<=_than X

    proof

      thus p is_less_than X implies (p % ) is_<=_than X

      proof

        assume

         A1: for q st q in X holds p [= q;

        let p9;

        

         A2: (( % p9) % ) = ( % p9);

        assume p9 in X;

        then p [= ( % p9) by A1;

        hence thesis by A2, Th7;

      end;

      assume

       A3: for q9 st q9 in X holds (p % ) <= q9;

      let q;

      assume q in X;

      then (p % ) <= (q % ) by A3;

      hence thesis by Th7;

    end;

    theorem :: LATTICE3:29

    p9 is_<=_than X iff ( % p9) is_less_than X

    proof

      (( % p9) % ) = ( % p9);

      hence thesis by Th28;

    end;

    theorem :: LATTICE3:30

    

     Th30: X is_less_than p iff X is_<=_than (p % )

    proof

      thus X is_less_than p implies X is_<=_than (p % )

      proof

        assume

         A1: for q st q in X holds q [= p;

        let p9;

        

         A2: (( % p9) % ) = ( % p9);

        assume p9 in X;

        then ( % p9) [= p by A1;

        hence thesis by A2, Th7;

      end;

      assume

       A3: for q9 st q9 in X holds q9 <= (p % );

      let q;

      assume q in X;

      then (q % ) <= (p % ) by A3;

      hence thesis by Th7;

    end;

    theorem :: LATTICE3:31

    

     Th31: X is_<=_than p9 iff X is_less_than ( % p9)

    proof

      (( % p9) % ) = ( % p9);

      hence thesis by Th30;

    end;

    registration

      let A be complete non empty Poset;

      cluster ( latt A) -> complete;

      coherence

      proof

        A is with_suprema with_infima by Th12;

        then

         A1: the RelStr of A = ( LattPOSet ( latt A)) by Def15;

        set B = ( LattPOSet ( latt A));

        ( latt A) is complete

        proof

          let X;

          consider a be Element of A such that

           A2: X is_<=_than a and

           A3: for b be Element of A st X is_<=_than b holds a <= b by Def12;

          reconsider a9 = a as Element of B by A1;

          take p = ( % a9);

          

           A4: (p % ) = p;

          thus X is_less_than p

          proof

            let q be Element of ( latt A);

            reconsider b = q as Element of A by A1;

            assume q in X;

            then b <= a by A2;

            then [b, a] in the InternalRel of A;

            then (q % ) <= a9 by A1;

            hence q [= p by A4, Th7;

          end;

          let q be Element of ( latt A);

          assume X is_less_than q;

          then

           A5: X is_<=_than (q % ) by Th30;

          reconsider b = (q % ) as Element of A by A1;

          X is_<=_than b

          proof

            let c be Element of A;

            reconsider c9 = c as Element of B by A1;

            assume c in X;

            then c9 <= (q % ) by A5;

            then [c, b] in the InternalRel of the RelStr of A by A1;

            hence c <= b;

          end;

          then a <= b by A3;

          then [a, b] in the InternalRel of A;

          then a9 <= (q % ) by A1;

          hence thesis by A4, Th7;

        end;

        hence thesis;

      end;

    end

    definition

      let L be non empty LattStr;

      let X be set;

      :: LATTICE3:def21

      func "\/" (X,L) -> Element of L means

      : Def21: X is_less_than it & for r be Element of L st X is_less_than r holds it [= r;

      existence by A1, Def18;

      uniqueness

      proof

        let p1,p2 be Element of L such that

         A2: X is_less_than p1 and

         A3: for r be Element of L st X is_less_than r holds p1 [= r and

         A4: X is_less_than p2 and

         A5: for r be Element of L st X is_less_than r holds p2 [= r;

        

         A6: p1 [= p2 by A3, A4;

        p2 [= p1 by A2, A5;

        hence thesis by A1, A6, LATTICES: 8;

      end;

    end

    definition

      let L be non empty LattStr, X be set;

      :: LATTICE3:def22

      func "/\" (X,L) -> Element of L equals ( "\/" ({ p where p be Element of L : p is_less_than X },L));

      correctness ;

    end

    notation

      let L be non empty LattStr, X be Subset of L;

      synonym "\/" X for "\/" (X,L);

      synonym "/\" X for "/\" (X,L);

    end

    reserve C for complete Lattice,

a,a9,b,b9,c,d for Element of C,

X,Y for set;

    theorem :: LATTICE3:32

    

     Th32: ( "\/" ({ (a "/\" b) : b in X },C)) [= (a "/\" ( "\/" (X,C)))

    proof

      set Y = { (a "/\" b) : b in X };

      Y is_less_than (a "/\" ( "\/" (X,C)))

      proof

        let c;

        assume c in Y;

        then

        consider b such that

         A1: c = (a "/\" b) and

         A2: b in X;

        X is_less_than ( "\/" (X,C)) by Def21;

        then b [= ( "\/" (X,C)) by A2;

        hence thesis by A1, LATTICES: 9;

      end;

      hence thesis by Def21;

    end;

    theorem :: LATTICE3:33

    

     Th33: C is \/-distributive iff for X, a holds (a "/\" ( "\/" (X,C))) [= ( "\/" ({ (a "/\" b) : b in X },C))

    proof

      thus C is \/-distributive implies for X, a holds (a "/\" ( "\/" (X,C))) [= ( "\/" ({ (a "/\" b) : b in X },C))

      proof

        assume

         A1: for X holds for a, b, c st X is_less_than a & (for d st X is_less_than d holds a [= d) & { (b "/\" a9) : a9 in X } is_less_than c & for d st { (b "/\" b9) : b9 in X } is_less_than d holds c [= d holds (b "/\" a) [= c;

        let X, a;

        set Y = { (a "/\" b) : b in X };

        

         A2: X is_less_than ( "\/" (X,C)) by Def21;

        

         A3: for d st X is_less_than d holds ( "\/" (X,C)) [= d by Def21;

        

         A4: Y is_less_than ( "\/" (Y,C)) by Def21;

        for d st Y is_less_than d holds ( "\/" (Y,C)) [= d by Def21;

        hence thesis by A1, A2, A3, A4;

      end;

      assume

       A5: for X, a holds (a "/\" ( "\/" (X,C))) [= ( "\/" ({ (a "/\" b) : b in X },C));

      let X;

      let a, b, c;

      assume

       A6: X is_less_than a & (for d st X is_less_than d holds a [= d) & { (b "/\" a9) : a9 in X } is_less_than c & for d st { (b "/\" b9) : b9 in X } is_less_than d holds c [= d;

      then

       A7: a = ( "\/" (X,C)) by Def21;

      c = ( "\/" ({ (b "/\" a9) : a9 in X },C)) by A6, Def21;

      hence (b "/\" a) [= c by A5, A7;

    end;

    theorem :: LATTICE3:34

    

     Th34: a = ( "/\" (X,C)) iff a is_less_than X & for b st b is_less_than X holds b [= a

    proof

      set Y = { b : b is_less_than X };

      

       A1: a = ( "/\" (X,C)) iff Y is_less_than a & for c st Y is_less_than c holds a [= c by Def21;

      thus a = ( "/\" (X,C)) implies a is_less_than X & for b st b is_less_than X holds b [= a

      proof

        assume

         A2: a = ( "/\" (X,C));

        then

         A3: Y is_less_than a by Def21;

        thus a is_less_than X

        proof

          let b such that

           A4: b in X;

          Y is_less_than b

          proof

            let c;

            assume c in Y;

            then ex d be Element of C st c = d & d is_less_than X;

            hence thesis by A4;

          end;

          hence thesis by A2, Def21;

        end;

        let b;

        assume b is_less_than X;

        then b in Y;

        hence thesis by A3;

      end;

      assume that

       A5: a is_less_than X and

       A6: for b st b is_less_than X holds b [= a;

      

       A7: Y is_less_than a

      proof

        let b;

        assume b in Y;

        then ex c st b = c & c is_less_than X;

        hence thesis by A6;

      end;

      a in Y by A5;

      hence thesis by A1, A7;

    end;

    theorem :: LATTICE3:35

    

     Th35: (a "\/" ( "/\" (X,C))) [= ( "/\" ({ (a "\/" b) : b in X },C))

    proof

      set Y = { (a "\/" b) : b in X };

      Y is_greater_than (a "\/" ( "/\" (X,C)))

      proof

        let c;

        assume c in Y;

        then

        consider b such that

         A1: c = (a "\/" b) and

         A2: b in X;

        X is_greater_than ( "/\" (X,C)) by Th34;

        then ( "/\" (X,C)) [= b by A2;

        hence thesis by A1, FILTER_0: 1;

      end;

      hence thesis by Th34;

    end;

    theorem :: LATTICE3:36

    

     Th36: C is /\-distributive iff for X, a holds ( "/\" ({ (a "\/" b) : b in X },C)) [= (a "\/" ( "/\" (X,C)))

    proof

      thus C is /\-distributive implies for X, a holds ( "/\" ({ (a "\/" b) : b in X },C)) [= (a "\/" ( "/\" (X,C)))

      proof

        assume

         A1: for X holds for a, b, c st X is_greater_than a & (for d st X is_greater_than d holds d [= a) & { (b "\/" a9) : a9 in X } is_greater_than c & for d st { (b "\/" b9) : b9 in X } is_greater_than d holds d [= c holds c [= (b "\/" a);

        let X, a;

        set Y = { (a "\/" b) : b in X };

        

         A2: X is_greater_than ( "/\" (X,C)) by Th34;

        

         A3: for d st X is_greater_than d holds d [= ( "/\" (X,C)) by Th34;

        

         A4: Y is_greater_than ( "/\" (Y,C)) by Th34;

        for d st Y is_greater_than d holds d [= ( "/\" (Y,C)) by Th34;

        hence thesis by A1, A2, A3, A4;

      end;

      assume

       A5: for X, a holds ( "/\" ({ (a "\/" b) : b in X },C)) [= (a "\/" ( "/\" (X,C)));

      let X;

      let a, b, c;

      assume

       A6: X is_greater_than a & (for d st X is_greater_than d holds d [= a) & { (b "\/" a9) : a9 in X } is_greater_than c & for d st { (b "\/" b9) : b9 in X } is_greater_than d holds d [= c;

      then

       A7: a = ( "/\" (X,C)) by Th34;

      c = ( "/\" ({ (b "\/" a9) : a9 in X },C)) by A6, Th34;

      hence c [= (b "\/" a) by A5, A7;

    end;

    theorem :: LATTICE3:37

    ( "\/" (X,C)) = ( "/\" ({ a : a is_greater_than X },C))

    proof

      set Y = { a : a is_greater_than X };

      

       A1: ( "\/" (X,C)) is_less_than Y

      proof

        let a;

        assume a in Y;

        then ex b st a = b & b is_greater_than X;

        hence thesis by Def21;

      end;

      X is_less_than ( "\/" (X,C)) by Def21;

      then ( "\/" (X,C)) in Y;

      then for b st b is_less_than Y holds b [= ( "\/" (X,C));

      hence thesis by A1, Th34;

    end;

    theorem :: LATTICE3:38

    

     Th38: a in X implies a [= ( "\/" (X,C)) & ( "/\" (X,C)) [= a

    proof

      assume

       A1: a in X;

      X is_less_than ( "\/" (X,C)) by Def21;

      hence a [= ( "\/" (X,C)) by A1;

      { b : b is_less_than X } is_less_than a

      proof

        let c;

        assume c in { b : b is_less_than X };

        then ex b st c = b & b is_less_than X;

        hence c [= a by A1;

      end;

      hence thesis by Def21;

    end;

    theorem :: LATTICE3:39

    

     Th39: a is_less_than X implies a [= ( "/\" (X,C))

    proof

      assume a is_less_than X;

      then a in { b : b is_less_than X };

      hence thesis by Th38;

    end;

    theorem :: LATTICE3:40

    

     Th40: a in X & X is_less_than a implies ( "\/" (X,C)) = a

    proof

      assume that

       A1: a in X and

       A2: X is_less_than a;

      

       A3: ( "\/" (X,C)) [= a by A2, Def21;

      a [= ( "\/" (X,C)) by A1, Th38;

      hence thesis by A3, LATTICES: 8;

    end;

    theorem :: LATTICE3:41

    

     Th41: a in X & a is_less_than X implies ( "/\" (X,C)) = a

    proof

      assume that

       A1: a in X and

       A2: a is_less_than X;

      

       A3: ( "/\" (X,C)) [= a by A1, Th38;

      a [= ( "/\" (X,C)) by A2, Th39;

      hence thesis by A3, LATTICES: 8;

    end;

    theorem :: LATTICE3:42

    ( "\/" {a}) = a & ( "/\" {a}) = a

    proof

      

       A1: a in {a} by TARSKI:def 1;

       {a} is_less_than a

      proof

        let b;

        assume b in {a};

        hence b [= a by TARSKI:def 1;

      end;

      hence ( "\/" {a}) = a by A1, Th40;

      a is_less_than {a}

      proof

        let b;

        assume b in {a};

        hence a [= b by TARSKI:def 1;

      end;

      hence thesis by A1, Th41;

    end;

    theorem :: LATTICE3:43

    (a "\/" b) = ( "\/" {a, b}) & (a "/\" b) = ( "/\" {a, b})

    proof

      

       A1: {a, b} is_less_than (a "\/" b)

      proof

        let c;

        assume

         A2: c in {a, b};

        

         A3: a [= (a "\/" b) by LATTICES: 5;

        b [= (b "\/" a) by LATTICES: 5;

        hence thesis by A2, A3, TARSKI:def 2;

      end;

      

       A4: a in {a, b} by TARSKI:def 2;

      

       A5: b in {a, b} by TARSKI:def 2;

      now

        let c;

        assume

         A6: {a, b} is_less_than c;

        then

         A7: a [= c by A4;

        b [= c by A5, A6;

        hence (a "\/" b) [= c by A7, FILTER_0: 6;

      end;

      hence (a "\/" b) = ( "\/" {a, b}) by A1, Def21;

      (a "/\" b) is_less_than {a, b}

      proof

        let c;

        assume c in {a, b};

        then c = a or c = b & (b "/\" a) = (a "/\" b) by TARSKI:def 2;

        hence thesis by LATTICES: 6;

      end;

      then

       A8: (a "/\" b) in { c : c is_less_than {a, b} };

      { c : c is_less_than {a, b} } is_less_than (a "/\" b)

      proof

        let d be Element of C;

        assume d in { c : c is_less_than {a, b} };

        then

         A9: ex c st d = c & c is_less_than {a, b};

        then

         A10: d [= a by A4;

        d [= b by A5, A9;

        hence thesis by A10, FILTER_0: 7;

      end;

      hence thesis by A8, Th40;

    end;

    theorem :: LATTICE3:44

    a = ( "\/" ({ b : b [= a },C)) & a = ( "/\" ({ c : a [= c },C))

    proof

      set X = { b : b [= a }, Y = { c : a [= c };

      

       A1: a in X;

      

       A2: a in Y;

      X is_less_than a

      proof

        let b;

        assume b in X;

        then ex c st b = c & c [= a;

        hence thesis;

      end;

      hence a = ( "\/" (X,C)) by A1, Th40;

      a is_less_than Y

      proof

        let b;

        assume b in Y;

        then ex c st b = c & a [= c;

        hence thesis;

      end;

      hence thesis by A2, Th41;

    end;

    theorem :: LATTICE3:45

    

     Th45: X c= Y implies ( "\/" (X,C)) [= ( "\/" (Y,C)) & ( "/\" (Y,C)) [= ( "/\" (X,C))

    proof

      assume

       A1: X c= Y;

      X is_less_than ( "\/" (Y,C))

      proof

        let a;

        assume

         A2: a in X;

        Y is_less_than ( "\/" (Y,C)) by Def21;

        hence thesis by A1, A2;

      end;

      hence ( "\/" (X,C)) [= ( "\/" (Y,C)) by Def21;

      ( "/\" (Y,C)) is_less_than X

      proof

        let a;

        assume

         A3: a in X;

        ( "/\" (Y,C)) is_less_than Y by Th34;

        hence thesis by A1, A3;

      end;

      hence thesis by Th34;

    end;

    theorem :: LATTICE3:46

    

     Th46: ( "\/" (X,C)) = ( "\/" ({ a : ex b st a [= b & b in X },C)) & ( "/\" (X,C)) = ( "/\" ({ b : ex a st a [= b & a in X },C))

    proof

      set Y = { a : ex b st a [= b & b in X }, Z = { a : ex b st b [= a & b in X };

      X is_less_than ( "\/" (Y,C))

      proof

        let a;

        assume a in X;

        then a in Y;

        hence thesis by Th38;

      end;

      then

       A1: ( "\/" (X,C)) [= ( "\/" (Y,C)) by Def21;

      Y is_less_than ( "\/" (X,C))

      proof

        let a;

        assume a in Y;

        then ex b st a = b & ex c st b [= c & c in X;

        then

        consider c such that

         A2: a [= c and

         A3: c in X;

        c [= ( "\/" (X,C)) by A3, Th38;

        hence thesis by A2, LATTICES: 7;

      end;

      then ( "\/" (Y,C)) [= ( "\/" (X,C)) by Def21;

      hence ( "\/" (X,C)) = ( "\/" (Y,C)) by A1, LATTICES: 8;

      X is_greater_than ( "/\" (Z,C))

      proof

        let a;

        assume a in X;

        then a in Z;

        hence thesis by Th38;

      end;

      then

       A4: ( "/\" (Z,C)) [= ( "/\" (X,C)) by Th34;

      Z is_greater_than ( "/\" (X,C))

      proof

        let a;

        assume a in Z;

        then ex b st a = b & ex c st c [= b & c in X;

        then

        consider c such that

         A5: c [= a and

         A6: c in X;

        ( "/\" (X,C)) [= c by A6, Th38;

        hence thesis by A5, LATTICES: 7;

      end;

      then ( "/\" (X,C)) [= ( "/\" (Z,C)) by Th34;

      hence thesis by A4, LATTICES: 8;

    end;

    theorem :: LATTICE3:47

    (for a st a in X holds ex b st a [= b & b in Y) implies ( "\/" (X,C)) [= ( "\/" (Y,C))

    proof

      assume

       A1: for a st a in X holds ex b st a [= b & b in Y;

      X is_less_than ( "\/" (Y,C))

      proof

        let a;

        assume a in X;

        then

        consider b such that

         A2: a [= b and

         A3: b in Y by A1;

        b [= ( "\/" (Y,C)) by A3, Th38;

        hence thesis by A2, LATTICES: 7;

      end;

      hence thesis by Def21;

    end;

    theorem :: LATTICE3:48

    X c= ( bool the carrier of C) implies ( "\/" (( union X),C)) = ( "\/" ({ ( "\/" Y) where Y be Subset of C : Y in X },C))

    proof

      set Z = { ( "\/" Y) where Y be Subset of C : Y in X };

      Z is_less_than ( "\/" (( union X),C))

      proof

        let a;

        assume a in Z;

        then

        consider Y be Subset of C such that

         A1: a = ( "\/" Y) and

         A2: Y in X;

        Y c= ( union X) by A2, ZFMISC_1: 74;

        hence thesis by A1, Th45;

      end;

      then

       A3: ( "\/" (Z,C)) [= ( "\/" (( union X),C)) by Def21;

      set V = { a : ex b st a [= b & b in Z };

      assume

       A4: X c= ( bool the carrier of C);

      ( union X) c= V

      proof

        let x be object;

        assume x in ( union X);

        then

        consider Y such that

         A5: x in Y and

         A6: Y in X by TARSKI:def 4;

        reconsider Y as Subset of C by A4, A6;

        reconsider a = x as Element of C by A4, A5, A6;

        

         A7: a [= ( "\/" Y) by A5, Th38;

        ( "\/" Y) in Z by A6;

        hence thesis by A7;

      end;

      then ( "\/" (( union X),C)) [= ( "\/" (V,C)) by Th45;

      then ( "\/" (( union X),C)) [= ( "\/" (Z,C)) by Th46;

      hence thesis by A3, LATTICES: 8;

    end;

    theorem :: LATTICE3:49

    C is 0_Lattice & ( Bottom C) = ( "\/" ( {} ,C))

    proof

       A1:

      now

        let a;

         {} is_less_than (( "\/" ( {} ,C)) "/\" a);

        then

         A2: ( "\/" ( {} ,C)) [= (( "\/" ( {} ,C)) "/\" a) by Def21;

        

         A3: (( "\/" ( {} ,C)) "/\" a) [= ( "\/" ( {} ,C)) by LATTICES: 6;

        hence (( "\/" ( {} ,C)) "/\" a) = ( "\/" ( {} ,C)) by A2, LATTICES: 8;

        thus (a "/\" ( "\/" ( {} ,C))) = ( "\/" ( {} ,C)) by A2, A3, LATTICES: 8;

      end;

      then C is lower-bounded;

      hence thesis by A1, LATTICES:def 16;

    end;

    theorem :: LATTICE3:50

    C is 1_Lattice & ( Top C) = ( "\/" (the carrier of C,C))

    proof

      set j = ( "\/" (the carrier of C,C));

       A1:

      now

        let a;

        

         A2: j [= (j "\/" a) by LATTICES: 5;

        

         A3: (j "\/" a) [= j by Th38;

        hence (j "\/" a) = j by A2, LATTICES: 8;

        thus (a "\/" j) = j by A2, A3, LATTICES: 8;

      end;

      then C is upper-bounded;

      hence thesis by A1, LATTICES:def 17;

    end;

    theorem :: LATTICE3:51

    

     Th51: C is I_Lattice implies (a => b) = ( "\/" ({ c : (a "/\" c) [= b },C))

    proof

      set X = { a9 : (a "/\" a9) [= b };

      assume

       A1: C is I_Lattice;

      then (a "/\" (a => b)) [= b by FILTER_0:def 7;

      then

       A2: (a => b) in X;

      X is_less_than (a => b)

      proof

        let c;

        assume c in X;

        then ex a9 st c = a9 & (a "/\" a9) [= b;

        hence c [= (a => b) by A1, FILTER_0:def 7;

      end;

      hence thesis by A2, Th40;

    end;

    theorem :: LATTICE3:52

    C is I_Lattice implies C is \/-distributive

    proof

      assume

       A1: C is I_Lattice;

      now

        let X, a;

        set Y = { (a "/\" a9) : a9 in X }, b = ( "\/" (X,C)), c = ( "\/" (Y,C)), Z = { b9 : (a "/\" b9) [= c };

        X is_less_than (a => c)

        proof

          let b9;

          assume b9 in X;

          then (a "/\" b9) in Y;

          then (a "/\" b9) [= c by Th38;

          then

           A2: b9 in Z;

          (a => c) = ( "\/" (Z,C)) by A1, Th51;

          hence thesis by A2, Th38;

        end;

        then b [= (a => c) by Def21;

        then

         A3: (a "/\" b) [= (a "/\" (a => c)) by LATTICES: 9;

        (a "/\" (a => c)) [= c by A1, FILTER_0:def 7;

        hence (a "/\" b) [= c by A3, LATTICES: 7;

      end;

      hence thesis by Th33;

    end;

    theorem :: LATTICE3:53

    for D be complete \/-distributive Lattice, a be Element of D holds (a "/\" ( "\/" (X,D))) = ( "\/" ({ (a "/\" b1) where b1 be Element of D : b1 in X },D)) & (( "\/" (X,D)) "/\" a) = ( "\/" ({ (b2 "/\" a) where b2 be Element of D : b2 in X },D))

    proof

      let D be complete \/-distributive Lattice, a be Element of D;

      

       A1: ( "\/" ({ (a "/\" b) where b be Element of D : b in X },D)) [= (a "/\" ( "\/" (X,D))) by Th32;

      

       A2: (a "/\" ( "\/" (X,D))) [= ( "\/" ({ (a "/\" b) where b be Element of D : b in X },D)) by Th33;

      hence (a "/\" ( "\/" (X,D))) = ( "\/" ({ (a "/\" b) where b be Element of D : b in X },D)) by A1, LATTICES: 8;

      deffunc U( Element of D) = ($1 "/\" a);

      deffunc V( Element of D) = (a "/\" $1);

      defpred X[ set] means $1 in X;

      

       A3: for b be Element of D holds V(b) = U(b);

      { V(b) where b be Element of D : X[b] } = { U(c) where c be Element of D : X[c] } from FRAENKEL:sch 5( A3);

      hence thesis by A1, A2, LATTICES: 8;

    end;

    theorem :: LATTICE3:54

    for D be complete /\-distributive Lattice, a be Element of D holds (a "\/" ( "/\" (X,D))) = ( "/\" ({ (a "\/" b1) where b1 be Element of D : b1 in X },D)) & (( "/\" (X,D)) "\/" a) = ( "/\" ({ (b2 "\/" a) where b2 be Element of D : b2 in X },D))

    proof

      let D be complete /\-distributive Lattice, a be Element of D;

      defpred X[ set] means $1 in X;

      

       A1: ( "/\" ({ (a "\/" b) where b be Element of D : b in X },D)) [= (a "\/" ( "/\" (X,D))) by Th36;

      

       A2: (a "\/" ( "/\" (X,D))) [= ( "/\" ({ (a "\/" b) where b be Element of D : b in X },D)) by Th35;

      hence (a "\/" ( "/\" (X,D))) = ( "/\" ({ (a "\/" b) where b be Element of D : b in X },D)) by A1, LATTICES: 8;

      deffunc U( Element of D) = ($1 "\/" a);

      deffunc V( Element of D) = (a "\/" $1);

      

       A3: for b be Element of D holds V(b) = U(b);

      { V(b) where b be Element of D : X[b] } = { U(c) where c be Element of D : X[c] } from FRAENKEL:sch 5( A3);

      hence thesis by A1, A2, LATTICES: 8;

    end;

    scheme :: LATTICE3:sch1

    SingleFraenkel { A() -> set , B() -> non empty set , P[ set] } :

{ A() where a be Element of B() : P[a] } = {A()}

      provided

       A1: ex a be Element of B() st P[a];

      thus { A() where a be Element of B() : P[a] } c= {A()}

      proof

        let x be object;

        assume x in { A() where a be Element of B() : P[a] };

        then ex a be Element of B() st x = A() & P[a];

        hence thesis by TARSKI:def 1;

      end;

      let x be object;

      assume x in {A()};

      then x = A() by TARSKI:def 1;

      hence thesis by A1;

    end;

    scheme :: LATTICE3:sch2

    FuncFraenkel { B() -> non empty set , C() -> non empty set , A( set) -> Element of C() , f() -> Function , P[ set] } :

(f() .: { A(x) where x be Element of B() : P[x] }) = { (f() . A(x)) where x be Element of B() : P[x] }

      provided

       A1: C() c= ( dom f());

      set f = f();

      thus (f .: { A(x) where x be Element of B() : P[x] }) c= { (f . A(x)) where x be Element of B() : P[x] }

      proof

        let y be object;

        assume y in (f .: { A(x) where x be Element of B() : P[x] });

        then

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

         A2: z in { A(x) where x be Element of B() : P[x] } and

         A3: y = (f . z) by FUNCT_1:def 6;

        ex x be Element of B() st z = A(x) & P[x] by A2;

        hence thesis by A3;

      end;

      let y be object;

      assume y in { (f . A(x)) where x be Element of B() : P[x] };

      then

      consider x be Element of B() such that

       A4: y = (f . A(x)) and

       A5: P[x];

      

       A6: A(x) in ( dom f) by A1;

      A(x) in { A(z) where z be Element of B() : P[z] } by A5;

      hence thesis by A4, A6, FUNCT_1:def 6;

    end;

     Lm3:

    now

      let D be non empty set, f be Function of ( bool D), D such that

       A1: for a be Element of D holds (f . {a}) = a and

       A2: for X be Subset-Family of D holds (f . (f .: X)) = (f . ( union X));

      defpred X[ object, object] means (f . {$1, $2}) = $2;

      consider R be Relation of D such that

       A3: for x,y be object holds [x, y] in R iff x in D & y in D & X[x, y] from RELSET_1:sch 1;

      

       A4: ( dom f) = ( bool D) by FUNCT_2:def 1;

       A5:

      now

        let x,y be Subset of D;

        

        thus (f . {(f . x), (f . y)}) = (f . (f .: {x, y})) by A4, FUNCT_1: 60

        .= (f . ( union {x, y})) by A2

        .= (f . (x \/ y)) by ZFMISC_1: 75;

      end;

      

       A6: for x,y be Element of D, X be Subset of D st y in X holds (f . (X \/ {x})) = (f . { (f . {t, x}) where t be Element of D : t in X })

      proof

        let x,y be Element of D, X be Subset of D such that

         A7: y in X;

        set Y = { {t, x} where t be Element of D : t in X };

        

         A8: (X \/ {x}) = ( union Y)

        proof

          thus (X \/ {x}) c= ( union Y)

          proof

            let s be object;

            assume s in (X \/ {x});

            then s in X & X c= D or s in {x} by XBOOLE_0:def 3;

            then s in X & s is Element of D or s = x by TARSKI:def 1;

            then s in {s, x} & {s, x} in Y or s in {y, x} & {y, x} in Y by A7, TARSKI:def 2;

            hence thesis by TARSKI:def 4;

          end;

          let s be object;

          assume s in ( union Y);

          then

          consider Z be set such that

           A9: s in Z and

           A10: Z in Y by TARSKI:def 4;

          consider t be Element of D such that

           A11: Z = {t, x} and

           A12: t in X by A10;

          s = t or s = x & x in {x} by A9, A11, TARSKI:def 1, TARSKI:def 2;

          hence thesis by A12, XBOOLE_0:def 3;

        end;

        Y c= ( bool D)

        proof

          let s be object;

          reconsider ss = s as set by TARSKI: 1;

          assume s in Y;

          then ss c= (X \/ {x}) by A8, ZFMISC_1: 74;

          then ss c= D by XBOOLE_1: 1;

          hence thesis;

        end;

        then

        reconsider Y as Subset-Family of D;

        defpred X[ set] means $1 in X;

        deffunc U( Element of D) = {$1, x};

        

         A13: ( bool D) c= ( dom f) by FUNCT_2:def 1;

        (f .: { U(t) where t be Element of D : X[t] }) = { (f . U(t)) where t be Element of D : X[t] } from FuncFraenkel( A13);

        then (f . ( union Y)) = (f . { (f . {t, x}) where t be Element of D : t in X }) by A2;

        hence thesis by A8;

      end;

      

       A14: R is_reflexive_in D

      proof

        let x be object;

        assume

         A15: x in D;

        

        then x = (f . {x}) by A1

        .= (f . {x, x}) by ENUMSET1: 29;

        hence thesis by A3, A15;

      end;

      

       A16: R is_antisymmetric_in D

      proof

        let x,y be object;

        assume that x in D and y in D and

         A17: [x, y] in R and

         A18: [y, x] in R;

        (f . {x, y}) = y by A3, A17;

        hence thesis by A3, A18;

      end;

      

       A19: R is_transitive_in D

      proof

        let x,y,z be object;

        assume that

         A20: x in D and

         A21: y in D and

         A22: z in D and

         A23: [x, y] in R and

         A24: [y, z] in R;

        reconsider a = x, b = y, c = z as Element of D by A20, A21, A22;

        

         A25: (f . {x, y}) = y by A3, A23;

        

         A26: (f . {y, z}) = z by A3, A24;

        

        then (f . {a, c}) = (f . {(f . {a}), (f . {b, c})}) by A1

        .= (f . ( {a} \/ {b, c})) by A5

        .= (f . {a, b, c}) by ENUMSET1: 2

        .= (f . ( {a, b} \/ {c})) by ENUMSET1: 3

        .= (f . {(f . {a, b}), (f . {c})}) by A5

        .= c by A1, A25, A26;

        hence thesis by A3;

      end;

      

       A27: ( dom R) = D by A14, ORDERS_1: 13;

      ( field R) = D by A14, ORDERS_1: 13;

      then

      reconsider R as Order of D by A14, A16, A19, A27, PARTFUN1:def 2, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16;

      set A = RelStr (# D, R #);

      A is complete

      proof

        let X;

        reconsider Y = (X /\ D) as Subset of D by XBOOLE_1: 17;

        reconsider a = (f . Y) as Element of A;

        take a;

        thus X is_<=_than a

        proof

          let b be Element of A;

          assume b in X;

          then b in Y by XBOOLE_0:def 4;

          then ( {b} \/ Y) = Y by ZFMISC_1: 40;

          

          then a = (f . {(f . {b}), a}) by A5

          .= (f . {b, a}) by A1;

          hence [b, a] in the InternalRel of A by A3;

        end;

        let b be Element of A such that

         A28: X is_<=_than b;

        

         A29: (f . {a, b}) = (f . {a, (f . {b})}) by A1

        .= (f . (Y \/ {b})) by A5;

        now

          per cases ;

            suppose

             A30: Y <> {} ;

            set s = the Element of Y;

            reconsider s as Element of D by A30, TARSKI:def 3;

            deffunc U( Element of D) = (f . {$1, b});

            deffunc V( Element of D) = b;

            defpred X[ set] means $1 in Y;

            

             A31: for t be Element of D st X[t] holds U(t) = V(t)

            proof

              let t be Element of D;

              reconsider s = t as Element of A;

              reconsider y = b as Element of D;

              assume t in Y;

              then t in X by XBOOLE_0:def 4;

              then s <= b by A28;

              then [t, y] in R;

              hence thesis by A3;

            end;

            

             A32: s in Y by A30;

            then

             A33: ex t be Element of D st X[t];

            { U(t) where t be Element of D : X[t] } = { V(t) where t be Element of D : X[t] } from FRAENKEL:sch 6( A31)

            .= { b where t be Element of D : X[t] }

            .= {b} from SingleFraenkel( A33);

            

            hence (f . {a, b}) = (f . {b}) by A6, A29, A32

            .= b by A1;

          end;

            suppose Y = {} ;

            hence (f . {a, b}) = b by A1, A29;

          end;

        end;

        hence [a, b] in the InternalRel of A by A3;

      end;

      then

      reconsider A as complete strict non empty Poset;

      take L = ( latt A);

      

       A34: A is with_suprema with_infima by Th12;

      then

       A35: A = ( LattPOSet L) by Def15;

      hence carr(L) = D;

      let X be Subset of L;

      reconsider Y = X as Subset of D by A35;

      reconsider a = (f . Y) as Element of ( LattPOSet L) by A34, Def15;

      set p = ( % a);

      X is_<=_than a

      proof

        let b be Element of ( LattPOSet L);

        reconsider y = b as Element of D by A34, Def15;

        assume b in X;

        then

         A36: X = ( {b} \/ X) by ZFMISC_1: 40;

        (f . {y, (f . Y)}) = (f . {(f . {y}), (f . Y)}) by A1

        .= a by A5, A36;

        hence [b, a] in the InternalRel of ( LattPOSet L) by A3, A35;

      end;

      then

       A37: X is_less_than p by Th31;

      now

        let q be Element of L;

        reconsider y = q as Element of D by A35;

        reconsider b = y as Element of ( LattPOSet L);

        assume X is_less_than q;

        then

         A38: X is_<=_than (q % ) by Th30;

        

         A39: (f . {(f . Y), b}) = (f . {(f . Y), (f . {y})}) by A1

        .= (f . (Y \/ {b})) by A5;

        now

          per cases ;

            suppose

             A40: Y <> {} ;

            set s = the Element of Y;

            reconsider s as Element of D by A40, TARSKI:def 3;

            deffunc U( Element of D) = (f . {$1, b});

            deffunc V( Element of D) = b;

            defpred X[ set] means $1 in Y;

            

             A41: for t be Element of D st X[t] holds U(t) = V(t)

            proof

              let t be Element of D;

              reconsider s = t as Element of ( LattPOSet L) by A34, Def15;

              assume t in Y;

              then s <= b by A38;

              then [t, y] in R by A35;

              hence thesis by A3;

            end;

            

             A42: s in Y by A40;

            then

             A43: ex t be Element of D st X[t];

            { U(t) where t be Element of D : X[t] } = { V(t) where t be Element of D : X[t] } from FRAENKEL:sch 6( A41)

            .= { b where t be Element of D : X[t] }

            .= {b} from SingleFraenkel( A43);

            

            hence (f . {a, b}) = (f . {b}) by A6, A39, A42

            .= b by A1;

          end;

            suppose Y = {} ;

            hence (f . {a, b}) = b by A1, A39;

          end;

        end;

        then [a, b] in the InternalRel of ( LattPOSet L) by A3, A35;

        then

         A44: a <= b;

        

         A45: (p % ) = p;

        (q % ) = b;

        hence p [= q by A44, A45, Th7;

      end;

      hence ( "\/" X) = (f . X) by A37, Def21;

    end;

    theorem :: LATTICE3:55

    for D be non empty set, f be Function of ( bool D), D st (for a be Element of D holds (f . {a}) = a) & for X be Subset-Family of D holds (f . (f .: X)) = (f . ( union X)) holds ex L be complete strict Lattice st the carrier of L = D & for X be Subset of L holds ( "\/" X) = (f . X) by Lm3;