The Mizar article:

Homomorphisms of Lattices, Finite Join and Finite Meet

by
Jolanta Kamienska, and
Jaroslaw Stanislaw Walijewski

Received July 14, 1993

Copyright (c) 1993 Association of Mizar Users

MML identifier: LATTICE4
[ MML identifier index ]


environ

 vocabulary TARSKI, SETFAM_1, BOOLE, LATTICES, FILTER_0, GROUP_6, FUNCT_1,
      MOD_4, RELAT_1, WELLORD1, FILTER_1, ZF_LANG, SUBSET_1, FINSUB_1,
      LATTICE2, SETWISEO, BINOP_1, FUNCOP_1, VECTSP_1, LATTICE4, HAHNBAN;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, ORDINAL1,
      FUNCT_1, FUNCT_2, BINOP_1, FINSUB_1, STRUCT_0, LATTICES, LATTICE2,
      FILTER_0, FUNCOP_1, SETWISEO, GRCAT_1, WELLORD1, FILTER_1;
 constructors BINOP_1, LATTICE2, SETWISEO, GRCAT_1, WELLORD1, FILTER_1,
      DOMAIN_1, XBOOLE_0, TOPS_2;
 clusters LATTICES, FILTER_0, STRUCT_0, FINSUB_1, RELSET_1, SUBSET_1, XBOOLE_0,
      ZFMISC_1;
 requirements BOOLE, SUBSET;
 definitions TARSKI, FILTER_0, LATTICES, XBOOLE_0;
 theorems LATTICES, ZFMISC_1, FUNCT_2, FILTER_0, SETFAM_1, ORDERS_2, TARSKI,
      TMAP_1, SETWISEO, LATTICE2, FUNCOP_1, FILTER_1, WELLORD1, RELAT_1,
      XBOOLE_0, XBOOLE_1;
 schemes FUNCT_2, SETWISEO, COMPLSP1, XBOOLE_0;

begin :: Preliminaries

reserve x,y,X,X1,Y,Z for set;

theorem
   union Y c= Z & X in Y implies X c= Z
 proof
  assume that
A1: union Y c= Z and
A2: X in Y;
  thus X c= Z
   proof let x be set;
    assume x in X;
     then x in union Y by A2,TARSKI:def 4;
    hence x in Z by A1;
   end;
 end;

theorem
    union INTERSECTION(X,Y) = union X /\ union Y
 proof
  thus union INTERSECTION(X,Y) c= union X /\ union Y by SETFAM_1:39;
  let x be set;
  assume x in union X /\ union Y;
then A1:   x in union X & x in union Y by XBOOLE_0:def 3;
   then consider X0 being set such that
A2:  x in X0 & X0 in X by TARSKI:def 4;
   consider Y0 being set such that
A3:  x in Y0 & Y0 in Y by A1,TARSKI:def 4;
A4: X0 /\ Y0 in INTERSECTION(X,Y) by A2,A3,SETFAM_1:def 5;
     x in X0 /\ Y0 by A2,A3,XBOOLE_0:def 3;
  hence x in union INTERSECTION(X,Y) by A4,TARSKI:def 4;
 end;

theorem
    for X st X <> {} &
   for Z st Z <> {} & Z c= X &
    Z is c=-linear
     ex Y st Y in X & for X1 st X1 in Z holds X1 c= Y
   ex Y st Y in X & for Z st Z in X & Z <> Y holds not Y c= Z
proof
  let X such that
  A1: X <> {} &
     for Z st Z <> {} & Z c= X & Z is c=-linear
         ex Y st Y in X & for X1 st X1 in Z holds X1 c= Y;
    for Z st Z c= X & Z is c=-linear
      ex Y st Y in X & for X1 st X1 in Z holds X1 c= Y
  proof
    let Z such that
    A2: Z c= X & Z is c=-linear;
    per cases;
     suppose A3: Z = {};
        consider Y being Element of X;
          for X1 st X1 in Z holds X1 c= Y by A3;
        hence ex Y st Y in X & for X1 st X1 in Z holds X1 c= Y by A1;
     suppose Z <> {};
        hence ex Y st Y in X & for X1 st X1 in Z holds X1 c= Y by A1,A2;
  end;
  hence thesis by A1,ORDERS_2:77;
end;

begin :: Lattice Theory

reserve L for Lattice;
reserve F,H for Filter of L;
reserve p,q,r for Element of L;

theorem
    <.L.) is prime
 proof
   let p,q;
     p in the carrier of L & q in the carrier of L & p"\/"q in the carrier of L
;
   hence p"\/"q in<.L.) iff p in <.L.) or q in <.L.) by FILTER_0:def 2;
 end;

theorem
   F c= <.F \/ H.) & H c= <.F \/ H.)
 proof
   A1:   F c= F \/ H & H c= F \/ H by XBOOLE_1:7;
     F \/ H c= <.F \/ H.) by FILTER_0:def 5;
   hence thesis by A1,XBOOLE_1:1;
 end;

theorem
    p in <.<.q.) \/ F.) implies ex r st r in F & q "/\" r [= p
 proof
   assume A1:   p in <.<.q.) \/ F.);
     <.<.q.) \/ F.)={r : ex p',q' being Element of L st
                  p'"/\"q' [= r & p' in <.q.) & q' in F} by FILTER_0:48;
   then ex r st r=p & ex p',q' being Element of L st
                         p'"/\"q' [= r & p' in <.q.) & q' in F by A1;
   then consider p',q' being Element of L such that
   A2:       p' "/\" q' [= p & p' in <.q.) & q' in F;
     q [= p' by A2,FILTER_0:18;
   then q "/\" q' [= p' "/\" q' by LATTICES:27;
   then q "/\" q' [= p by A2,LATTICES:25;
   hence thesis by A2;
 end;

reserve L1, L2 for Lattice;
reserve a1,b1 for Element of L1;
reserve a2 for Element of L2;

definition let L1,L2;
 mode Homomorphism of L1,L2 ->
  Function of the carrier of L1, the carrier of L2 means
 :Def1: it.(a1 "\/" b1) = it.a1 "\/" it.b1 &
       it.(a1 "/\" b1) = it.a1 "/\" it.b1;
 existence
 proof
   consider b being Element of L2;
   defpred P[set,set] means for a1 st $1=a1 holds $2=b;
   A1:   now let x be Element of L1;
          take b;
          thus P[x,b];
        end;
   consider f being Function of the carrier of L1,the carrier of L2 such that
   A2:     for x being Element of L1 holds P[x,f.x]
                                                           from FuncExD(A1);
   take f;
     now
     let a1,b1;
     thus f.(a1 "\/" b1) = b by A2
                      .= b "\/" b by LATTICES:17
                      .= f.a1 "\/" b by A2
                      .= f.a1 "\/" f.b1 by A2;
     thus f.(a1 "/\" b1) = b by A2
                      .= b "/\" b by LATTICES:18
                      .= f.a1 "/\" b by A2
                      .= f.a1 "/\" f.b1 by A2;
   end;
   hence thesis;
 end;
end;

reserve f for Homomorphism of L1,L2;

theorem Th7:
 a1 [= b1 implies f.a1 [= f.b1
 proof
   assume A1:a1 [= b1;
   thus f.a1 [= f.b1
   proof
     thus f.a1 "\/" f.b1 = f.(a1 "\/" b1) by Def1
                      .=f.b1 by A1,LATTICES:def 3;
   end;
 end;

definition let L1,L2;
           let f be Function of the carrier of L1, the carrier of L2;
 attr f is monomorphism means
  :Def2:   f is one-to-one;
 attr f is epimorphism means
  :Def3:   rng f = the carrier of L2;
end;

theorem
Th8: f is monomorphism implies (a1 [= b1 iff (f.a1) [= (f.b1))
 proof
   assume f is monomorphism;
   then A1: f is one-to-one by Def2;
   reconsider f as Function of the carrier of L1,the carrier of L2;
        f.a1 [= f.b1 implies a1 [= b1
   proof
     assume f.a1 [= f.b1;
     then f.a1 "\/" f.b1 = f.b1 by LATTICES:def 3;
     then f.(a1 "\/" b1) =f.b1 by Def1;
     hence a1 "\/" b1 = b1 by A1,FUNCT_2:25;
   end;
   hence thesis by Th7;
 end;

theorem Th9:
 for f being Function of the carrier of L1, the carrier of L2 holds
  f is epimorphism implies (for a2 ex a1 st a2 = f.a1)
 proof
   let f be Function of the carrier of L1, the carrier of L2;
   assume A1: f is epimorphism;
   reconsider g = f as Function of the carrier of L1,the carrier of L2;
A2:rng g = the carrier of L2 by A1,Def3;
     now let a2 be Element of L2;
     consider x be set such that
A3:  x in the carrier of L1 & g.x = a2 by A2,FUNCT_2:17;
     thus ex a1 st g.a1 = a2 by A3;
   end;
   hence thesis;
 end;

definition
  let L1,L2,f;
 attr f is isomorphism means
  :Def4:  f is monomorphism epimorphism;
end;

definition let L1,L2;
 redefine pred L1,L2 are_isomorphic means
      ex f st f is isomorphism;
 compatibility
 proof
   thus L1,L2 are_isomorphic implies ex f st f is isomorphism
   proof
     assume L1,L2 are_isomorphic;
     then LattRel L1, LattRel L2 are_isomorphic by FILTER_1:def 9;
     then consider F being Function such that
A1:  F is_isomorphism_of LattRel L1, LattRel L2 by WELLORD1:def 8;
     set R = LattRel L1, S = LattRel L2;
A2:  field S = the carrier of L2 & field R = the carrier of L1 by FILTER_1:33;
A3:  dom F = field R & rng F = field S & F is one-to-one &
     for a,b being set holds [a,b] in R iff
       a in field R & b in field R & [F.a,F.b] in S by A1,WELLORD1:def 7;
     then reconsider F as Function of the carrier of L1,
                                 the carrier of L2 by A2,FUNCT_2:3;
       now let a1,b1 be Element of L1;
       reconsider a1'=a1,b1'=b1 as Element of L1;
A4:     F is epimorphism by A2,A3,Def3;
       thus F.(a1 "\/" b1) = F.a1 "\/" F.b1
       proof
         consider k1 being Element of L1 such that
A5:      F.a1 "\/" F.b1 = F.k1 by A4,Th9;
           F.a1 [= F.k1 & F.b1 [= F.k1 by A5,LATTICES:22;
         then [F.a1,F.k1] in LattRel L2 & [F.b1,F.k1] in LattRel L2 by FILTER_1
:32;
         then [a1,k1] in LattRel L1 & [b1,k1] in LattRel L1 by A1,A2,WELLORD1:
def 7;
         then a1 [= k1 & b1 [= k1 by FILTER_1:32;
         then a1 "\/" b1 [= k1 by FILTER_0:6;
         then [a1 "\/" b1,k1] in R by FILTER_1:32;
         then [F.(a1 "\/" b1),F.k1] in LattRel L2 by A1,WELLORD1:def 7;
then A6:       F.(a1 "\/" b1) [= F.a1 "\/" F.b1 by A5,FILTER_1:32;
           a1' [= a1' "\/" b1' by LATTICES:22;
         then [a1,a1 "\/" b1] in R by FILTER_1:32;
         then [F.a1,F.(a1 "\/" b1)] in S by A1,WELLORD1:def 7;
then A7:       F.a1' [= F.(a1' "\/" b1') by FILTER_1:32;
           b1' [= a1' "\/" b1' by LATTICES:22;
         then [b1,a1 "\/" b1] in R by FILTER_1:32;
         then [F.b1,F.(a1 "\/" b1)] in S by A1,WELLORD1:def 7;
         then F.b1' [= F.(a1' "\/" b1') by FILTER_1:32;
         then F.a1 "\/" F.b1 [= F.(a1 "\/" b1) by A7,FILTER_0:6;
         hence thesis by A6,LATTICES:26;
       end;
       thus F.(a1 "/\" b1) = F.a1 "/\" F.b1
       proof
         consider k1 being Element of L1 such that
A8:      F.a1 "/\" F.b1 = F.k1 by A4,Th9;
           F.k1 [= F.a1 & F.k1 [= F.b1 by A8,LATTICES:23;
         then [F.k1,F.a1] in LattRel L2 & [F.k1,F.b1] in LattRel L2 by FILTER_1
:32;
         then [k1,a1] in LattRel L1 & [k1,b1] in LattRel L1 by A1,A2,WELLORD1:
def 7;
         then k1 [= a1 & k1 [= b1 by FILTER_1:32;
         then k1 [= a1 "/\" b1 by FILTER_0:7;
         then [k1,a1 "/\" b1] in LattRel L1 by FILTER_1:32;
         then [F.k1,F.(a1 "/\" b1)] in LattRel L2 by A1,WELLORD1:def 7;
then A9:       F.a1 "/\" F.b1 [= F.(a1 "/\" b1) by A8,FILTER_1:32;
           a1' "/\" b1' [= a1' by LATTICES:23;
         then [a1 "/\" b1,a1] in R by FILTER_1:32;
         then [F.(a1 "/\" b1),F.a1] in S by A1,WELLORD1:def 7;
then A10:       F.(a1' "/\" b1') [= F.a1' by FILTER_1:32;
           a1' "/\" b1' [= b1' by LATTICES:23;
         then [a1 "/\" b1,b1] in R by FILTER_1:32;
         then [F.(a1 "/\" b1),F.b1] in S by A1,WELLORD1:def 7;
         then F.(a1' "/\" b1') [= F.b1' by FILTER_1:32;
         then F.(a1 "/\" b1) [= F.a1 "/\" F.b1 by A10,FILTER_0:7;
         hence thesis by A9,LATTICES:26;
       end;
     end;
     then reconsider F as Homomorphism of L1,L2 by Def1;
     take F;
       F is monomorphism epimorphism by A2,A3,Def2,Def3;
     hence thesis by Def4;
   end;
   given f such that
A11:f is isomorphism;
A12: f is monomorphism epimorphism by A11,Def4;
then A13:f is one-to-one by Def2;
   set R = LattRel L1, S = LattRel L2;
A14:dom f = the carrier of L1 by FUNCT_2:def 1
        .= field R by FILTER_1:33;
A15:rng f = the carrier of L2 by A12,Def3
        .= field S by FILTER_1:33;
     for a,b be set holds [a,b] in R iff
   a in field R & b in field R & [f.a,f.b] in S
   proof
     let a,b be set;
     hereby assume A16: [a,b] in R;
       hence a in field R & b in field R by RELAT_1:30;
       then reconsider a'=a,b'=b as Element of L1 by FILTER_1:33
;
         a' [= b' by A16,FILTER_1:32;
       then f.a' [= f.b' by A12,Th8;
       hence [f.a,f.b] in S by FILTER_1:32;
     end;
     assume A17:a in field R & b in field R & [f.a,f.b] in S;
     then reconsider a'=a,b'=b as Element of L1 by FILTER_1:33;
       f.a' [= f.b' by A17,FILTER_1:32;
     then a' [= b' by A12,Th8;
     hence thesis by FILTER_1:32;
   end;
   then f is_isomorphism_of LattRel L1, LattRel L2 by A13,A14,A15,WELLORD1:def
7;
   then LattRel L1, LattRel L2 are_isomorphic by WELLORD1:def 8;
   hence thesis by FILTER_1:def 9;
 end;
end;

definition
let L1,L2,f;
 pred f preserves_implication means
  :Def6:   f.(a1 => b1) = (f.a1) => (f.b1);
 pred f preserves_top means
  :Def7:   f.(Top L1) = Top L2;
 pred f preserves_bottom means
  :Def8:   f.(Bottom L1) = Bottom L2;
 pred f preserves_complement means
  :Def9:   f.(a1`) = (f.a1)`;
end;

definition let L;
 mode ClosedSubset of L -> Subset of L means
 :Def10: p in it & q in it implies p "/\" q in it & p "\/" q in it;
 existence
 proof
     the carrier of L c= the carrier of L;
   then reconsider F = the carrier of L as non empty Subset of L
;
   take F;
   thus thesis;
 end;
end;

theorem Th10:
  the carrier of L is ClosedSubset of L
 proof
     the carrier of L c= the carrier of L;
   then reconsider F=the carrier of L as Subset of L;
     p in F & q in F implies p "/\" q in F & p "\/" q in F;
   hence the carrier of L is ClosedSubset of L by Def10;
 end;

definition let L;
 cluster non empty ClosedSubset of L;
  existence
 proof
     the carrier of L is ClosedSubset of L by Th10;
   hence thesis;
 end;
end;

theorem
    for F being Filter of L holds F is ClosedSubset of L
 proof
   let F be Filter of L;
     for p,q st p in F & q in F holds
   p "/\" q in F & p "\/" q in F by FILTER_0:10,def 1;
   hence F is ClosedSubset of L by Def10;
 end;

 reserve B for Finite_Subset of the carrier of L;

definition let L,B;
 canceled;

  func FinJoin B -> Element of L equals
  :Def12: FinJoin (B,id L);
 correctness;
  func FinMeet B -> Element of L equals
  :Def13: FinMeet (B,id L);
 correctness;
end;

canceled 2;

theorem Th14:
  FinMeet B = (the L_meet of L) $$ (B,id L)
 proof
   thus FinMeet B = FinMeet(B,id L) by Def13
                 .= (the L_meet of L) $$ (B,id L) by LATTICE2:def 4;
 end;

theorem Th15:
   FinJoin B = (the L_join of L) $$ (B,id L)
 proof
   thus FinJoin B = FinJoin(B,id L) by Def12
                 .= (the L_join of L) $$ (B,id L) by LATTICE2:def 3;
 end;

theorem Th16:
  FinJoin {p} = p
 proof set J=the L_join of L;
   A1:   J is commutative associative by LATTICE2:27,29;
   thus FinJoin {p} =(the L_join of L) $$ ({p},id L) by Th15
                   .= (id L).p by A1,SETWISEO:26
                   .= p by TMAP_1:91;
 end;

theorem Th17:
 FinMeet {p} = p
 proof
   set M = the L_meet of L;
   A1:   M is commutative associative by LATTICE2:31,32;
   thus FinMeet {p} = M $$ ({p},id L) by Th14
                   .= (id L).p by A1,SETWISEO:26
                   .= p by TMAP_1:91;
 end;

begin :: Distributive Lattices

reserve DL for distributive Lattice;
reserve f for Homomorphism of DL,L2;

theorem Th18:
  f is epimorphism implies L2 is distributive
 proof
   assume A1:f is epimorphism;
   thus L2 is distributive
   proof
     let a,b,c be Element of L2;
     consider a' be Element of DL such that
     A2:      f.a'=a by A1,Th9;
     consider b' be Element of DL such that
     A3:      f.b'=b by A1,Th9;
     consider c' be Element of DL such that
     A4:      f.c'=c by A1,Th9;
     thus a"/\"(b"\/"c) = a"/\"f.(b'"\/"c') by A3,A4,Def1
                     .= f.(a'"/\"(b'"\/"c')) by A2,Def1
                     .=f.((a'"/\"b')"\/"(a'"/\"c')) by LATTICES:def 11
                     .=f.(a'"/\"b')"\/"f.(a'"/\"c') by Def1
                     .=(a"/\"b)"\/"f.(a'"/\"c') by A2,A3,Def1
                     .=(a"/\"b)"\/"(a"/\"c) by A2,A4,Def1;
   end;
 end;

begin :: Lower-bounded Lattices

reserve 0L for lower-bounded Lattice,
        B,B1,B2 for Finite_Subset of the carrier of 0L,
        b for Element of 0L;

theorem Th19:
 for f being Homomorphism of 0L,L2 st f is epimorphism
  holds L2 is lower-bounded & f preserves_bottom
 proof let f be Homomorphism of 0L,L2;
   assume A1:   f is epimorphism;
   set r = f.(Bottom 0L);
   A2:  now let a2 be Element of L2;
         consider a1 be Element of 0L such that
         A3:      f.a1 = a2 by A1,Th9;
         thus r"/\"a2 = f.(Bottom 0L "/\" a1) by A3,Def1
                    .= r by LATTICES:40;
         hence a2"/\"r = r;
       end;
   thus L2 is lower-bounded
   proof
     take r;
     thus thesis by A2;
   end;
   then Bottom L2=r by A2,LATTICES:def 16;
   hence thesis by Def8;
 end;

reserve f for UnOp of the carrier of 0L;

theorem Th20:
  FinJoin(B \/ {b},f) = FinJoin (B,f) "\/" f.b
 proof
   set J= the L_join of 0L;
   A1:   J is idempotent & J is commutative & J is associative
        & J has_a_unity by LATTICE2:26,27,29,67;
   thus FinJoin (B \/ {b},f) = J $$ (B \/ {b},f) by LATTICE2:def 3
             .= J.(J $$ (B,f),f.b) by A1,SETWISEO:41
             .= J $$ (B,f) "\/" f.b by LATTICES:def 1
             .= FinJoin (B,f) "\/" f.b by LATTICE2:def 3;
 end;

theorem Th21:
  FinJoin(B \/ {b}) = FinJoin B "\/" b
 proof
   thus FinJoin(B \/ {b}) = FinJoin(B \/ {b},id 0L) by Def12
                        .=FinJoin (B,id 0L) "\/" (id 0L).b by Th20
                        .=FinJoin (B,id 0L) "\/" b by TMAP_1:91
                        .= FinJoin B "\/" b by Def12;
 end;

 theorem
    FinJoin B1 "\/" FinJoin B2 = FinJoin (B1 \/ B2)
 proof
   set J= the L_join of 0L;
   A1:   J is idempotent & J is commutative & J is associative
      & J has_a_unity by LATTICE2:26,27,29,67;
   thus FinJoin (B1 \/ B2) = J $$ (B1 \/ B2,id 0L) by Th15
                    .= J.(J $$ (B1,id 0L ),J $$ (B2,id 0L)) by A1,SETWISEO:42
                    .= J $$ (B1,id 0L) "\/" J $$ (B2,id 0L) by LATTICES:def 1
                    .= FinJoin B1 "\/" J $$ (B2,id 0L) by Th15
                    .=FinJoin B1 "\/" FinJoin B2 by Th15;
 end;

Lm1:
 for f being Function of the carrier of 0L , the carrier of 0L
 holds FinJoin ({}.the carrier of 0L,f) = Bottom 0L
 proof let f be Function of the carrier of 0L , the carrier of 0L;
   set J=the L_join of 0L;
   A1:   J is commutative & J is associative & J has_a_unity
                        by LATTICE2:27,29,67;
   thus FinJoin ({}.the carrier of 0L,f)
       = J $$ ({}.the carrier of 0L,f) by LATTICE2:def 3
      .= the_unity_wrt J by A1,SETWISEO:40
      .= Bottom 0L by LATTICE2:68;
 end;

theorem Th23:
  FinJoin {}.the carrier of 0L = Bottom 0L
 proof
   thus FinJoin {}.the carrier of 0L
                   = FinJoin ({}.the carrier of 0L,id 0L) by Def12
                  .= Bottom 0L by Lm1;
 end;

theorem
 Th24: for A being ClosedSubset of 0L st Bottom 0L in A
            for B holds B c= A implies FinJoin B in A
 proof
   let A be ClosedSubset of 0L;
   defpred X[Finite_Subset of the carrier of 0L] means
      $1 c= A implies FinJoin $1 in A;
   assume Bottom 0L in A;
   then
   A1: X[{}.the carrier of 0L] by Th23;
   A2:   for B1 being Finite_Subset of the carrier of 0L
          for p being Element of 0L st X[B1]
           holds X[B1 \/ {p}]
   proof
     let B1 be Finite_Subset of the carrier of 0L;
     let p be Element of 0L;
     assume A3:    B1 c=A implies FinJoin B1 in A;
     assume A4:    B1 \/ {p} c=A;
     then {p} c= A by XBOOLE_1:11;
     then p in A by ZFMISC_1:37;
     then FinJoin B1 "\/" p in A by A3,A4,Def10,XBOOLE_1:11;
     hence thesis by Th21;
   end;
   thus for B being Element of Fin the carrier of 0L
    holds X[B] from FinSubInd3(A1,A2);
 end;

begin :: Upper-bounded Lattices

reserve 1L for upper-bounded Lattice,
        B,B1,B2 for Finite_Subset of the carrier of 1L,
        b for Element of 1L;

theorem Th25:
  for f being Homomorphism of 1L,L2 st f is epimorphism
   holds L2 is upper-bounded & f preserves_top
 proof let f be Homomorphism of 1L,L2;
   assume A1:   f is epimorphism;
   set r = f.(Top 1L);
   A2:  now let a2 be Element of L2;
         consider a1 be Element of 1L such that
         A3:      f.a1 = a2 by A1,Th9;
         thus r"\/"a2 = f.(Top 1L "\/" a1) by A3,Def1
                    .= r by LATTICES:44;
         hence a2"\/"r = r;
       end;
   thus L2 is upper-bounded
   proof
     take r;
     thus thesis by A2;
   end;
   then Top L2=r by A2,LATTICES:def 17;
   hence thesis by Def7;
 end;

Lm2:
 for f being Function of the carrier of 1L, the carrier of 1L
 holds FinMeet ({}.the carrier of 1L,f) = Top 1L
 proof
  let f be Function of the carrier of 1L, the carrier of 1L;
   set M=the L_meet of 1L;
   A1:   M is commutative associative & M has_a_unity
                              by LATTICE2:31,32,73;
   thus FinMeet ({}.the carrier of 1L,f)
                     = M $$ ({}.the carrier of 1L,f) by LATTICE2:def 4
                    .= the_unity_wrt M by A1,SETWISEO:40
                    .= Top 1L by LATTICE2:74;
 end;

theorem Th26:
  FinMeet {}.the carrier of 1L = Top 1L
 proof
   thus FinMeet {}.the carrier of 1L
                      = FinMeet ({}.the carrier of 1L,id 1L) by Def13
                     .= Top 1L by Lm2;
 end;

reserve f,g for UnOp of the carrier of 1L;

theorem Th27:
   FinMeet(B \/ {b},f) = FinMeet (B,f) "/\" f.b
 proof
   set M= the L_meet of 1L;
   A1:   M is idempotent & M is commutative & M is associative
        & M has_a_unity by LATTICE2:30,31,32,73;
   thus FinMeet (B \/ {b},f) = M $$ (B \/ {b},f) by LATTICE2:def 4
                             .= M.(M $$ (B,f),f.b) by A1,SETWISEO:41
                             .= M $$ (B,f) "/\" f.b by LATTICES:def 2
                             .= FinMeet (B,f) "/\" f.b by LATTICE2:def 4;
 end;

theorem Th28:
  FinMeet(B \/ {b}) = FinMeet B "/\" b
 proof
   thus FinMeet(B \/ {b}) = FinMeet(B \/ {b},id 1L) by Def13
                        .=FinMeet (B,id 1L) "/\" (id 1L).b by Th27
                        .=FinMeet (B,id 1L) "/\" b by TMAP_1:91
                        .= FinMeet B "/\" b by Def13;
 end;

theorem Th29:
  FinMeet(f.:B,g) = FinMeet(B,g*f)
 proof
   set M= the L_meet of 1L;
   A1:    M is idempotent & M is commutative associative
       & M has_a_unity by LATTICE2:30,31,32,73;
   thus FinMeet(f.:B,g) = M$$(f.:B,g) by LATTICE2:def 4
                      .= M$$(B,g*f) by A1,SETWISEO:44
                      .= FinMeet(B,g*f)by LATTICE2:def 4;
 end;

theorem Th30:
 FinMeet B1 "/\" FinMeet B2 = FinMeet (B1 \/ B2)
 proof
   set M= the L_meet of 1L;
   A1:   M is idempotent & M is commutative & M is associative
      & M has_a_unity by LATTICE2:30,31,32,73;
   thus FinMeet (B1 \/ B2) = M $$ (B1 \/ B2,id 1L) by Th14
                    .= M.(M $$ (B1,id 1L ),M $$ (B2,id 1L)) by A1,SETWISEO:42
                    .= M $$ (B1,id 1L) "/\" M $$ (B2,id 1L) by LATTICES:def 2
                    .= FinMeet B1 "/\" M $$ (B2,id 1L) by Th14
                    .=FinMeet B1 "/\" FinMeet B2 by Th14;
 end;

theorem
Th31: for F being ClosedSubset of 1L st Top 1L in F
         for B holds B c= F implies FinMeet B in F
 proof
   let F be ClosedSubset of 1L;
   defpred X[Finite_Subset of the carrier of 1L] means
      $1 c= F implies FinMeet $1 in F;
   assume Top 1L in F;
   then
A1:  X[{}.the carrier of 1L] by Th26;
   A2:   for B1 being Finite_Subset of the carrier of 1L
          for p being Element of 1L st X[B1]
           holds X[B1 \/ {p}]
   proof
     let B1 be Finite_Subset of the carrier of 1L;
     let p be Element of 1L;
     assume A3:B1 c=F implies FinMeet B1 in F;
     assume A4:B1 \/ {p} c=F;
     then {p} c= F by XBOOLE_1:11;
     then p in F by ZFMISC_1:37;
     then FinMeet B1 "/\" p in F by A3,A4,Def10,XBOOLE_1:11;
     hence thesis by Th28;
   end;
   thus for B being Element of Fin  the carrier of 1L
      holds X[B] from FinSubInd3(A1,A2);
 end;

begin :: Distributive Upper-bounded Lattices

 reserve DL for distributive upper-bounded Lattice,
         B for Finite_Subset of the carrier of DL,
         p for Element of DL,
         f for UnOp of the carrier of DL;

  Lm3: (the L_join of DL).((the L_meet of DL) $$ (B,f),p) =
          (the L_meet of DL) $$ (B,(the L_join of DL) [:] (f,p))
 proof
   set J = the L_join of DL;
   set M = the L_meet of DL;
   A1:   M is idempotent & M is commutative & M is associative
                                by LATTICE2:30,31,32;
   A2:   J is_distributive_wrt M by LATTICE2:35;
     now per cases;
     suppose B<> {};
       hence J.(M $$ (B,f),p) = M $$ (B,J [:] (f,p)) by A1,A2,SETWISEO:37;
     suppose A3:   B = {};
       A4:  now let f;
             thus M $$ (B,f) = FinMeet({}.the carrier of DL,f) by A3,LATTICE2:
def 4
                    .=Top DL by Lm2;
           end;
      hence J.(M $$ (B,f),p) = J.(Top DL,p)
                           .= Top DL "\/" p by LATTICES:def 1
                           .= Top DL by LATTICES:44
                           .= M $$ (B,J [:] (f,p)) by A4;
   end;
   hence thesis;
 end;

theorem
Th32: FinMeet B "\/" p = FinMeet (((the L_join of DL)[:](id DL,p)).:B)
 proof
   set J = the L_join of DL;
   set M = the L_meet of DL;
   thus FinMeet B "\/" p =J.(FinMeet B,p) by LATTICES:def 1
                      .= J.(M $$ (B,id DL),p) by Th14
                      .= M $$ (B,J [:] (id DL,p)) by Lm3
                      .=FinMeet(B,J [:] (id DL,p)) by LATTICE2:def 4
                      .= FinMeet (B,(id DL)*(J [:] (id DL,p))) by TMAP_1:93
                      .= FinMeet ((J [:] (id DL,p)).:B,id DL) by Th29
                      .= FinMeet (((the L_join of DL)[:](id DL,p)).:
B) by Def13;
 end;

begin :: Implicative Lattices

reserve CL for C_Lattice;
reserve IL for implicative Lattice;
reserve f for Homomorphism of IL,CL;
reserve i,j,k for Element of IL;

theorem Th33:
  f.i "/\" f.(i => j) [= f.j
 proof
     i "/\" (i => j) [= j by FILTER_0:def 8;
   then f.(i "/\" (i => j)) [= f.j by Th7;
   hence thesis by Def1;
 end;

theorem Th34:
  f is monomorphism implies (f.i "/\" f.k [= f.j implies f.k [= f.(i => j))
 proof
   assume A1: f is monomorphism;
   hereby
     assume f.i "/\" f.k [= f.j;
     then f.(i "/\" k) [= f.j by Def1;
     then i "/\" k [= j by A1,Th8;
     then k [= (i => j) by FILTER_0:def 8;
     hence f.k [= f.(i => j) by Th7;
   end;
 end;

theorem
  f is isomorphism implies (CL is implicative & f preserves_implication)
 proof
   assume f is isomorphism;
   then A1: f is epimorphism monomorphism by Def4;
   thus CL is implicative
   proof
     let p,q be Element of CL;
     consider i such that A2: f.i=p by A1,Th9;
     consider j such that A3: f.j=q by A1,Th9;
     take r = f.(i => j);
     thus p "/\" r [= q by A2,A3,Th33;
     hereby let r1 be Element of CL;
       consider k such that
       A4:    f.k = r1 by A1,Th9;
       assume p "/\" r1 [= q;
       hence r1 [= r by A1,A2,A3,A4,Th34;
     end;
   end;
   then reconsider CL as implicative Lattice;
   reconsider f as Homomorphism of IL,CL;
       now let i,j;
       A5:  (f.i) "/\" f.(i => j) [= (f.j) by Th33;
         now let r1 be Element of CL;
         consider k such that
         A6:f.k=r1 by A1,Th9;
         assume (f.i) "/\" r1 [= (f.j);
         hence r1 [= f.(i => j) by A1,A6,Th34;
       end;
       hence (f.i) => (f.j) = f.(i => j) by A5,FILTER_0:def 8;
     end;
     hence thesis by Def6;
 end;

begin ::Boolean Lattices

reserve BL for Boolean Lattice;
reserve f for Homomorphism of BL,CL;
reserve A for non empty Subset of BL;
reserve a1,a,b,c,p,q for Element of BL;
reserve B,B0,B1,B2,B3,A1,A2 for Finite_Subset of the carrier of BL;

theorem
 Th36: (Top BL)`=Bottom BL
  proof
    set a=Bottom BL;
    thus (Top BL)` = (a "\/" a`)` by LATTICES:48
               .= a` "/\"a`` by LATTICES:51
               .= Bottom BL by LATTICES:47;
  end;

theorem
 Th37: (Bottom BL)`=Top BL
  proof
    set a=Top BL;
    thus (Bottom BL)` = (a "/\" a`)` by LATTICES:47
               .= a` "\/"a`` by LATTICES:50
               .= Top BL by LATTICES:48;
  end;

theorem
    f is epimorphism implies CL is Boolean & f preserves_complement
 proof
   assume A1: f is epimorphism;
   then A2: f preserves_top by Th25;
   A3: f preserves_bottom by A1,Th19;
   thus CL is bounded complemented;
   thus CL is distributive by A1,Th18;
   then reconsider CL as Boolean Lattice by LATTICES:def 20;
   reconsider f as Homomorphism of BL,CL;
     now let a1;
     A4:    f.(a1`)"\/"f.a1 =f.(a1` "\/" a1) by Def1
                        .=f.(Top BL) by LATTICES:48
                        .= Top CL by A2,Def7;
       f.(a1`)"/\"f.a1 = f.(a1` "/\" a1) by Def1
                  .=f.(Bottom BL) by LATTICES:47
                  .= Bottom CL by A3,Def8;
     then f.(a1`) is_a_complement_of f.a1 by A4,LATTICES:def 18;
     hence (f.a1)` = f.(a1`) by LATTICES:def 21;
   end;
   hence thesis by Def9;
 end;

definition let BL;
 mode Field of BL -> non empty Subset of BL means
 :Def14:  a in it & b in it implies a "/\" b in it & a` in it;
 existence
 proof
     the carrier of BL c= the carrier of BL;
   then reconsider F=the carrier of BL as non empty Subset of BL;
   take F; thus thesis;
 end;
end;

reserve F,H for Field of BL;

theorem
 Th39: a in F & b in F implies a "\/" b in F
 proof
   assume a in F & b in F;
   then a` in F & b` in F by Def14;
   then a` "/\" b` in F by Def14;
   then ( a"\/"b )` in F by LATTICES:51;
   then ( a"\/"b )`` in F by Def14;
   hence a"\/"b in F by LATTICES:49;
 end;

theorem
 Th40: a in F & b in F implies a => b in F
 proof
   assume A1: a in F & b in F;
   then a` in F by Def14;
   then a` "\/" b in F by A1,Th39;
   hence a => b in F by FILTER_0:55;
 end;

theorem
 Th41: the carrier of BL is Field of BL
 proof
     the carrier of BL c= the carrier of BL;
   then reconsider F=the carrier of BL as non empty Subset of BL;
        a in F & b in F implies a "/\" b in F & a` in F;
   hence the carrier of BL is Field of BL by Def14;
 end;

theorem
 Th42: F is ClosedSubset of BL
 proof
     for a,b st a in F & b in F holds
   a "/\" b in F & a "\/" b in F by Def14,Th39;
   hence F is ClosedSubset of BL by Def10;
 end;

definition let BL,A;
 func field_by A -> Field of BL means
 :Def15:  A c= it & for F st A c= F holds it c= F;
 existence
 proof
   defpred X[set] means $1 is Field of BL & A c= $1;
   consider X such that
A1:     Z in X iff Z in bool the carrier of BL & X[Z] from Separation;
   consider x being Element of A;
   A2: the carrier of BL c= the carrier of BL;
   reconsider x as Element of BL;
   A3:    A c= the carrier of BL & the carrier of BL is Field of BL &
           the carrier of BL in bool the carrier of BL by A2,Th41;
   then A4:    the carrier of BL in X by A1;
   A5:    X <> {} by A1,A3;
     now let Z;
     assume Z in X;
     then A c= Z by A1;
     hence x in Z by TARSKI:def 3;
   end;
   then reconsider F1 = meet X as non empty set by A5,SETFAM_1:def 1;
     F1 c= the carrier of BL
   proof
     let x;
     thus thesis by A4,SETFAM_1:def 1;
   end;
   then reconsider F1 as non empty Subset of BL;
     F1 is Field of BL
   proof
     let a,b;
     assume A6:   a in F1 & b in F1;
     A7:   a "/\" b in F1
     proof
         for Z st Z in X holds a "/\" b in Z
       proof
         let Z;
         assume A8:    Z in X;
         then A9:   Z is Field of BL by A1;
           a in Z & b in Z by A6,A8,SETFAM_1:def 1;
         hence thesis by A9,Def14;
       end;
       hence thesis by A5,SETFAM_1:def 1;
     end;
       a` in F1
     proof
         for Z st Z in X holds a` in Z
       proof
         let Z;
         assume A10:   Z in X;
         then A11:    Z is Field of BL by A1;
           a in Z by A6,A10,SETFAM_1:def 1;
         hence thesis by A11,Def14;
       end;
       hence thesis by A5,SETFAM_1:def 1;
     end;
     hence thesis by A7;
   end;
   then reconsider F = F1 as Field of BL;
   take F;
     for Z st Z in X holds A c= Z by A1;
   hence A c= F by A4,SETFAM_1:6;
   let H;
   assume A c= H;
   then H in X by A1;
   hence F c= H by SETFAM_1:4;
 end;
 uniqueness
 proof
   let F1,F2 be Field of BL such that
   A12:   A c= F1 & for F st A c= F holds F1 c= F and
   A13:   A c= F2 & for F st A c= F holds F2 c= F;
   thus F1 c= F2 & F2 c= F1 by A12,A13;
 end;
end;

definition let BL,A;
 func SetImp A -> Subset of BL equals
 :Def16:  { a => b : a in A & b in A};
 coherence
 proof
   set B={ a => b : a in A & b in A};
     B c= the carrier of BL
   proof
     let x;
     assume x in B;
     then ex p,q st x = p => q & p in A & q in A;
     hence x in the carrier of BL;
   end;
   hence thesis;
 end;
end;

definition let BL,A;
 cluster SetImp A -> non empty;
 coherence
 proof
   set B={ a => b : a in A & b in A};
   consider x being Element of A;
   reconsider x as Element of BL;
     x => x in B;
   then reconsider B as non empty set;
      B = SetImp A by Def16;
   hence thesis;
 end;
end;

theorem
 Th43: x in SetImp A iff ex p,q st x = p => q & p in A & q in A
 proof
     SetImp A = { a => b : a in A & b in A} by Def16;
   hence thesis;
 end;

theorem Th44: c in SetImp A iff ex p,q st c = p` "\/" q & p in A & q in A
 proof
   hereby assume c in SetImp A;
       then consider p,q such that
       A1:        c = p => q & p in A & q in A by Th43;
       take p,q;
       thus c = p` "\/" q & p in A & q in A by A1,FILTER_0:55;
   end;
   given p,q such that
   A2:    c = p` "\/" q & p in A & q in A;
     c = p => q by A2,FILTER_0:55;
   hence c in SetImp A by A2,Th43;
 end;

definition let BL;
 deffunc U(Element of BL) = $1`;
 func comp BL -> Function of the carrier of BL, the carrier of BL means
 :Def17:
     it.a = a`;
 existence
 proof
   consider f being Function of the carrier of BL,the carrier of BL such that
   A1:    for a holds f.a= U(a) from LambdaD;
   take f;
   thus thesis by A1;
  end;
  uniqueness
   proof
    thus for f1,f2 being Function of the carrier of BL,the carrier of BL st
     (for x being Element of BL holds f1.x = U(x)) &
     (for x being Element of BL holds f2.x = U(x))
    holds f1 = f2 from FuncDefUniq;
   end;
 end;

theorem Th45:
 FinJoin(B \/ {b},comp BL) = FinJoin (B,comp BL) "\/" b`
 proof
   thus FinJoin(B \/ {b},comp BL) = FinJoin(B,comp BL) "\/" (comp BL).b by Th20
                                .= FinJoin (B,comp BL) "\/" b` by Def17;
  end;

theorem
    (FinJoin B)` = FinMeet (B,comp BL)
 proof
   set M= the L_meet of BL;
   set J= the L_join of BL;
   A1:     M is idempotent commutative associative
       & M has_a_unity by LATTICE2:30,31,32,73;
   A2:     J is idempotent commutative associative
       & J has_a_unity by LATTICE2:26,27,29,67;
   A3:    (comp BL).(the_unity_wrt J) = the_unity_wrt M
   proof
     thus (comp BL).(the_unity_wrt J)= (the_unity_wrt J)` by Def17
                                    .=(Bottom BL )` by LATTICE2:68
                                    .=Top BL by Th37
                                    .= the_unity_wrt M by LATTICE2:74;
   end;
   A4:    for a,b being Element of BL
                  holds (comp BL).(J.(a,b))= M.((comp BL).a,(comp BL).b)
   proof
     let a,b be Element of BL;
     thus (comp BL).(J.(a,b))=(comp BL).(a"\/"b) by LATTICES:def 1
                            .=(a"\/"b)` by Def17
                            .=a`"/\"b` by LATTICES:51
                            .=M.(a`,b`) by LATTICES:def 2
                            .= M.((comp BL).a,b`) by Def17
                            .= M.((comp BL).a,(comp BL).b) by Def17;
   end;
   thus (FinJoin B)`= (J$$(B,id BL))` by Th15
                   .= (comp BL).(J$$(B,id BL)) by Def17
                   .= M$$(B,(comp BL)*(id BL)) by A1,A2,A3,A4,SETWISEO:45
                   .= M$$(B, comp BL) by TMAP_1:93
                   .= FinMeet(B, comp BL) by LATTICE2:def 4;
 end;

theorem
    FinMeet(B \/ {b},comp BL) = FinMeet (B,comp BL) "/\" b`
 proof
   thus FinMeet(B \/ {b},comp BL) =FinMeet (B,comp BL) "/\" (comp BL).b by Th27
                                .=FinMeet (B,comp BL) "/\" b` by Def17;
 end;

theorem Th48:
 (FinMeet B)` = FinJoin (B,comp BL)
 proof
   set M= the L_meet of BL;
   set J= the L_join of BL;
   A1:     M is idempotent commutative associative
       & M has_a_unity by LATTICE2:30,31,32,73;
   A2:     J is idempotent commutative associative
       & J has_a_unity by LATTICE2:26,27,29,67;
   A3:    (comp BL).(the_unity_wrt M) = the_unity_wrt J
   proof
     thus (comp BL).(the_unity_wrt M)= (the_unity_wrt M)` by Def17
                                    .=(Top BL )` by LATTICE2:74
                                    .=Bottom BL by Th36
                                    .= the_unity_wrt J by LATTICE2:68;
   end;
   A4:    for a,b being Element of BL
                  holds (comp BL).(M.(a,b))= J.((comp BL).a,(comp BL).b)
   proof
     let a,b be Element of BL;
     thus (comp BL).(M.(a,b))=(comp BL).(a"/\"b) by LATTICES:def 2
                            .=(a"/\"b)` by Def17
                            .=a`"\/"b` by LATTICES:50
                            .=J.(a`,b`) by LATTICES:def 1
                            .= J.((comp BL).a,b`) by Def17
                            .= J.((comp BL).a,(comp BL).b) by Def17;
   end;
   thus (FinMeet B)`= (M$$(B,id BL))` by Th14
                   .= (comp BL).(M$$(B,id BL)) by Def17
                   .= J$$(B,(comp BL)*(id BL)) by A1,A2,A3,A4,SETWISEO:45
                   .= J$$(B, comp BL) by TMAP_1:93
                   .= FinJoin(B, comp BL) by LATTICE2:def 3;
 end;

theorem
  Th49: for AF  being non empty ClosedSubset of BL st Bottom
BL in AF & Top BL in AF
     for B holds B c= SetImp AF implies
         ex B0 st B0 c= SetImp AF & FinJoin( B,comp BL) = FinMeet B0
 proof
   let AF be non empty ClosedSubset of BL such that A1:Bottom BL in AF & Top
BL in AF;
   let B;
   assume A2:       B c= SetImp AF;
   set C={ FinJoin A1 "\/" FinJoin(A2,comp BL): A1 c= AF & A2 c= AF};
   defpred X[Finite_Subset of the carrier of BL] means
      $1 c= SetImp AF implies
       ex B0 st B0 c= C & FinJoin($1,comp BL) = FinMeet B0;
   A3: X[{}.the carrier of BL]
   proof
   assume {}.the carrier of BL c= SetImp AF;
     take B0={Bottom BL};
     A4:   FinJoin ({}.the carrier of BL,comp BL)= Bottom BL by Lm1
                                               .=FinMeet {Bottom BL} by Th17;
       B0 c= C
     proof
       let x;
       assume x in B0;
       then A5:    x = Bottom BL by TARSKI:def 1;
         ex A1,A2 st
        x = FinJoin A1 "\/" FinJoin(A2,comp BL) & A1 c= AF & A2 c= AF
       proof
         take A1={Bottom BL};
         take A2={Top BL};
         thus x = Bottom BL "\/" Bottom BL by A5,LATTICES:17
                .= Bottom BL "\/" (Top BL)` by Th36
                .=FinJoin A1 "\/" (Top BL)` by Th16
                .=FinJoin A1 "\/" (FinMeet A2)` by Th17
                .=FinJoin A1 "\/" FinJoin (A2,comp BL) by Th48;
         thus A1 c= AF by A1,ZFMISC_1:37;
         thus A2 c= AF by A1,ZFMISC_1:37;
       end;
       hence x in C;
     end;
     hence thesis by A4;
   end;
   A6:  for B' being Finite_Subset of the carrier of BL,
         b being Element of BL st X[B']
          holds X[B' \/ {b}]
   proof
     let B' be Finite_Subset of the carrier of BL,
         b be Element of BL;
     assume A7:    (B' c= SetImp AF implies
           ex B1 st B1 c= C & FinJoin(B',comp BL) = FinMeet B1 );
     assume A8: B' \/ {b} c= SetImp AF;
     then A9:   B' c= SetImp AF & b in SetImp AF by SETWISEO:8;
     consider B1 such that
     A10:       B1 c= C & FinJoin(B',comp BL) = FinMeet B1 by A7,A8,SETWISEO:8;
     consider p,q such that
     A11:        b = p` "\/" q & p in AF & q in AF by A9,Th44;
     A12:    b` = p`` "/\" q` by A11,LATTICES:51
             .= p "/\" q` by LATTICES:49;
     set J = the L_join of BL;
     take (J[:](id BL,p)).:B1 \/ (J[:](id BL,q`)).:B1;
     A13:    FinJoin(B' \/ {b} ,comp BL) = FinMeet B1 "\/" (p "/\"
 q`) by A10,A12,Th45
         .= (FinMeet B1 "\/" p) "/\" (FinMeet B1 "\/" q`) by LATTICES:31
         .= FinMeet((J[:](id BL,p)).:B1) "/\" (FinMeet B1 "\/" q`) by Th32
         .= FinMeet((J[:](id BL,p)).:B1) "/\" FinMeet ((J[:]
(id BL,q`)).:B1) by Th32
         .= FinMeet ((J[:](id BL,p)).:B1 \/ (J[:](id BL,q`)).:B1) by Th30;
     A14:  for x,b holds x in (J[:](id BL,b)).:B1 implies ex a st
           a in B1 & x = a "\/" b
     proof
       let x,b;
       assume A15:    x in (J[:](id BL,b)).:B1;
         (J[:](id BL,b)).:B1 c= the carrier of BL by FUNCT_2:44;
       then reconsider x as Element of BL by A15;
       consider a such that
       A16:  a in B1 & x = (J[:](id BL,b)).a by A15,FUNCT_2:116;
         x = J.(id BL.a,b) by A16,FUNCOP_1:60
        .= J.(a,b) by TMAP_1:91
        .= a "\/" b by LATTICES:def 1;
       hence thesis by A16;
     end;
     A17:   (J[:](id BL,p)).:B1 c= C
     proof
       let x;
       assume x in (J[:](id BL,p)).:B1;
       then consider a such that
       A18:       a in B1 & x = a "\/" p by A14;
         a in C by A10,A18;
       then consider A1,A2 such that
       A19:      a = FinJoin A1 "\/" FinJoin(A2,comp BL) & A1 c= AF & A2 c= AF;
         ex A1',A2' being Finite_Subset of the carrier of BL st
         x = FinJoin A1' "\/" FinJoin (A2',comp BL) & A1' c= AF & A2' c= AF
       proof
         take A1'=A1 \/ {p};
         take A2'=A2;
              x = (FinJoin A1 "\/" p) "\/" FinJoin(A2,comp BL) by A18,A19,
LATTICES:def 5
               .= FinJoin(A1') "\/" FinJoin(A2',comp BL) by Th21;
        hence thesis by A11,A19,SETWISEO:8;
      end;
      hence x in C;
    end;
      (J[:](id BL,q`)).:B1 c= C
    proof
      let x;
      assume x in (J[:](id BL,q`)).:B1;
      then consider a such that
      A20:      a in B1 & x = a "\/" q` by A14;
        a in C by A10,A20;
      then consider A1,A2 such that
      A21:     a = FinJoin A1 "\/" FinJoin(A2,comp BL) & A1 c= AF & A2 c= AF;
        ex A1',A2' being Finite_Subset of the carrier of BL st
        x = FinJoin A1' "\/" FinJoin (A2',comp BL) & A1' c= AF & A2' c= AF
      proof
        take A1'=A1;
        take A2'=A2 \/ {q};
             x = FinJoin A1 "\/" (FinJoin(A2,comp BL) "\/" q`) by A20,A21,
LATTICES:def 5
              .= FinJoin(A1') "\/" FinJoin(A2',comp BL) by Th45;
        hence thesis by A11,A21,SETWISEO:8;
      end;
      hence x in C;
    end;
    hence thesis by A13,A17,XBOOLE_1:8;
  end;
    for B being Finite_Subset of the carrier of BL holds X[B]
     from FinSubInd3(A3,A6
);
  then consider B1 such that
  A22:      B1 c= C & FinJoin(B,comp BL) = FinMeet B1 by A2;
    C c= SetImp AF
  proof
    let x;
    assume x in C;
    then consider A1,A2 such that
    A23:      x = FinJoin A1 "\/" FinJoin(A2,comp BL) & A1 c= AF & A2 c= AF;
    consider p,q such that
    A24:      p = FinMeet A2 & q = FinJoin A1;
    A25:   p in AF & q in AF by A1,A23,A24,Th24,Th31;
      x = p` "\/" q by A23,A24,Th48;
    hence x in SetImp AF by A25,Th44;
  end;
  then B1 c= SetImp AF by A22,XBOOLE_1:1;
  hence thesis by A22;
 end;

theorem
    for AF being non empty ClosedSubset of BL st Bottom
BL in AF & Top BL in AF holds
    { FinMeet B : B c= SetImp AF } = field_by AF
 proof
   let AF be non empty ClosedSubset of BL such that
A1:  Bottom BL in AF & Top BL in AF;
   set A1= { FinMeet B :B c= SetImp AF };
   A2:     AF c= A1
   proof
     let x;
     assume A3:x in AF;
     then reconsider b=x as Element of BL;
     reconsider B = {b} as Finite_Subset of the carrier of BL;
       b = Bottom BL "\/" b by LATTICES:39
      .= (Top BL)` "\/" b by Th36;
     then b in SetImp AF by A1,A3,Th44;
     then A4:    B c= SetImp AF by ZFMISC_1:37;
       x = FinMeet B by Th17;
     hence x in A1 by A4;
   end;
     A1 c= the carrier of BL
   proof
     let x;
     assume x in A1;
     then consider B such that
     A5:    x = FinMeet B & B c= SetImp AF;
     thus x in the carrier of BL by A5;
   end;
   then reconsider A1 as non empty Subset of BL by A1,A2;
  A6:    A1 is Field of BL
  proof
    let p,q;
    assume A7:  p in A1 & q in A1;
    thus p "/\" q in A1
    proof
      consider B1 such that
      A8:      p=FinMeet B1 & B1 c= SetImp AF by A7;
      consider B2 such that
      A9:      q=FinMeet B2 & B2 c= SetImp AF by A7;
      consider B0 such that
      A10:      B0=B1 \/ B2;
      A11:  B0 c= SetImp AF by A8,A9,A10,XBOOLE_1:8;
        p "/\" q = FinMeet B0 by A8,A9,A10,Th30;
      hence thesis by A11;
    end;
    thus p` in A1
    proof
      consider B such that
      A12:     p=FinMeet B & B c= SetImp AF by A7;
        p` = FinJoin ( B,comp BL) by A12,Th48;
      then consider B0 such that
      A13:     B0 c= SetImp AF & p` = FinMeet B0 by A1,A12,Th49;
      thus thesis by A13;
    end;
  end;
    now let F;
    assume A14: AF c= F;
    thus A1 c= F
    proof
      let x;
      assume x in A1;
      then consider B such that
      A15:     x=FinMeet B & B c= SetImp AF;
A16:      SetImp AF c= F
      proof
        let y;
        assume y in SetImp AF;
        then consider p,q such that
        A17:     y = p => q & p in AF & q in AF by Th43;
        thus y in F by A14,A17,Th40;
      end;
      reconsider F1=F as ClosedSubset of BL by Th42;
        B c= F1 & Top BL in F1 by A1,A14,A15,A16,XBOOLE_1:1;
      hence x in F by A15,Th31;
    end;
  end;
  hence thesis by A2,A6,Def15;
end;

Back to top