lattice4.miz



    begin

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

    theorem :: LATTICE4:1

    for X st X <> {} & for Z st Z <> {} & Z c= X & Z is c=-linear holds ex Y st Y in X & for X1 st X1 in Z holds X1 c= Y holds 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 <> {} and

       A2: for Z st Z <> {} & Z c= X & Z is c=-linear holds 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 holds ex Y st Y in X & for X1 st X1 in Z holds X1 c= Y

      proof

        let Z such that

         A3: Z c= X & Z is c=-linear;

        per cases ;

          suppose

           A4: Z = {} ;

          set Y = the Element of X;

          for X1 st X1 in Z holds X1 c= Y by A4;

          hence thesis by A1;

        end;

          suppose Z <> {} ;

          hence thesis by A2, A3;

        end;

      end;

      hence thesis by A1, ORDERS_1: 65;

    end;

    begin

    reserve L for Lattice;

    reserve F,H for Filter of L;

    reserve p,q,r for Element of L;

    registration

      let L;

      cluster <.L.) -> prime;

      coherence ;

    end

    theorem :: LATTICE4:2

    F c= <.(F \/ H).) & H c= <.(F \/ H).)

    proof

      

       A1: (F \/ H) c= <.(F \/ H).) by FILTER_0:def 4;

      F c= (F \/ H) & H c= (F \/ H) by XBOOLE_1: 7;

      hence thesis by A1;

    end;

    theorem :: LATTICE4:3

    p in <.( <.q.) \/ F).) implies ex r st r in F & (q "/\" r) [= p

    proof

      

       A1: <.( <.q.) \/ F).) = { r : ex p9,q9 be Element of L st (p9 "/\" q9) [= r & p9 in <.q.) & q9 in F } by FILTER_0: 35;

      assume p in <.( <.q.) \/ F).);

      then ex r st r = p & ex p9,q9 be Element of L st (p9 "/\" q9) [= r & p9 in <.q.) & q9 in F by A1;

      then

      consider p9,q9 be Element of L such that

       A2: (p9 "/\" q9) [= p and

       A3: p9 in <.q.) and

       A4: q9 in F;

      q [= p9 by A3, FILTER_0: 15;

      then (q "/\" q9) [= (p9 "/\" q9) by LATTICES: 9;

      hence thesis by A2, A4, LATTICES: 7;

    end;

    reserve L1,L2 for Lattice;

    reserve a1,b1 for Element of L1;

    reserve a2 for Element of L2;

    definition

      let L1,L2 be non empty \/-SemiLattStr;

      let f be Function of L1, L2;

      :: LATTICE4:def1

      attr f is "\/"-preserving means

      : D1: for a,b be Element of L1 holds (f . (a "\/" b)) = ((f . a) "\/" (f . b));

    end

    definition

      let L1,L2 be non empty /\-SemiLattStr;

      let f be Function of L1, L2;

      :: LATTICE4:def2

      attr f is "/\"-preserving means

      : D2: for a,b be Element of L1 holds (f . (a "/\" b)) = ((f . a) "/\" (f . b));

    end

    registration

      let L1,L2 be meet-absorbing join-absorbing meet-commutative non empty LattStr;

      cluster "\/"-preserving "/\"-preserving for Function of L1, L2;

      existence

      proof

        set b = the Element of L2;

        defpred P[ set, set] means for a1 be Element of L1 st $1 = a1 holds $2 = b;

         A1:

        now

          let x be Element of L1;

          take b;

          thus P[x, b];

        end;

        consider f be Function of L1, L2 such that

         A2: for x be Element of L1 holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

        take f;

        thus f is "\/"-preserving

        proof

          let a1,b1 be Element of L1;

          

          thus (f . (a1 "\/" b1)) = b by A2

          .= (b "\/" b)

          .= ((f . a1) "\/" b) by A2

          .= ((f . a1) "\/" (f . b1)) by A2;

        end;

        let a1,b1 be Element of L1;

        

        thus (f . (a1 "/\" b1)) = b by A2

        .= (b "/\" b)

        .= ((f . a1) "/\" b) by A2

        .= ((f . a1) "/\" (f . b1)) by A2;

      end;

    end

    definition

      let L1,L2 be Lattice;

      mode Homomorphism of L1,L2 is "\/"-preserving "/\"-preserving Function of L1, L2;

    end

    reserve f for Homomorphism of L1, L2;

    theorem :: LATTICE4:4

    

     Th4: a1 [= b1 implies (f . a1) [= (f . b1) by D1;

    theorem :: LATTICE4:5

    

     Th5: f is one-to-one implies (a1 [= b1 iff (f . a1) [= (f . b1))

    proof

      assume

       A1: f is one-to-one;

      reconsider f as Function of L1, L2;

      (f . a1) [= (f . b1) implies a1 [= b1

      proof

        assume (f . a1) [= (f . b1);

        then ((f . a1) "\/" (f . b1)) = (f . b1);

        then (f . (a1 "\/" b1)) = (f . b1) by D1;

        hence (a1 "\/" b1) = b1 by A1, FUNCT_2: 19;

      end;

      hence thesis by Th4;

    end;

    theorem :: LATTICE4:6

    

     Th6: for f be Function of L1, L2 holds f is onto implies for a2 holds ex a1 st a2 = (f . a1)

    proof

      let f be Function of L1, L2;

      assume f is onto;

      then

       A1: ( rng f) = the carrier of L2 by FUNCT_2:def 3;

      now

        let a2 be Element of L2;

        ex x be object st x in the carrier of L1 & (f . x) = a2 by A1, FUNCT_2: 11;

        hence ex a1 st (f . a1) = a2;

      end;

      hence thesis;

    end;

    definition

      let L1, L2;

      :: original: are_isomorphic

      redefine

      :: LATTICE4:def3

      pred L1,L2 are_isomorphic means ex f st f is bijective;

      compatibility

      proof

        thus (L1,L2) are_isomorphic implies ex f st f is bijective

        proof

          set R = ( LattRel L1), S = ( LattRel L2);

          assume (L1,L2) are_isomorphic ;

          then (( LattRel L1),( LattRel L2)) are_isomorphic by FILTER_1:def 9;

          then

          consider F be Function such that

           A1: F is_isomorphism_of (( LattRel L1),( LattRel L2)) by WELLORD1:def 8;

          

           A2: ( dom F) = ( field R) by A1, WELLORD1:def 7;

          

           A3: ( field S) = the carrier of L2 & ( rng F) = ( field S) by A1, FILTER_1: 32, WELLORD1:def 7;

          

           A4: ( field R) = the carrier of L1 by FILTER_1: 32;

          then

          reconsider F as Function of L1, L2 by A2, A3, FUNCT_2: 1;

          now

            let a1,b1 be Element of L1;

            reconsider a19 = a1, b19 = b1 as Element of L1;

            

             A5: F is onto by A3, FUNCT_2:def 3;

            thus (F . (a1 "\/" b1)) = ((F . a1) "\/" (F . b1))

            proof

              b19 [= (a19 "\/" b19) by LATTICES: 5;

              then [b1, (a1 "\/" b1)] in R by FILTER_1: 31;

              then [(F . b1), (F . (a1 "\/" b1))] in S by A1, WELLORD1:def 7;

              then

               A6: (F . b19) [= (F . (a19 "\/" b19)) by FILTER_1: 31;

              consider k1 be Element of L1 such that

               A7: ((F . a1) "\/" (F . b1)) = (F . k1) by A5, Th6;

              (F . b1) [= (F . k1) by A7, LATTICES: 5;

              then [(F . b1), (F . k1)] in ( LattRel L2) by FILTER_1: 31;

              then [b1, k1] in ( LattRel L1) by A1, A4, WELLORD1:def 7;

              then

               A8: b1 [= k1 by FILTER_1: 31;

              (F . a1) [= (F . k1) by A7, LATTICES: 5;

              then [(F . a1), (F . k1)] in ( LattRel L2) by FILTER_1: 31;

              then [a1, k1] in ( LattRel L1) by A1, A4, WELLORD1:def 7;

              then a1 [= k1 by FILTER_1: 31;

              then (a1 "\/" b1) [= k1 by A8, FILTER_0: 6;

              then [(a1 "\/" b1), k1] in R by FILTER_1: 31;

              then [(F . (a1 "\/" b1)), (F . k1)] in ( LattRel L2) by A1, WELLORD1:def 7;

              then

               A9: (F . (a1 "\/" b1)) [= ((F . a1) "\/" (F . b1)) by A7, FILTER_1: 31;

              a19 [= (a19 "\/" b19) by LATTICES: 5;

              then [a1, (a1 "\/" b1)] in R by FILTER_1: 31;

              then [(F . a1), (F . (a1 "\/" b1))] in S by A1, WELLORD1:def 7;

              then (F . a19) [= (F . (a19 "\/" b19)) by FILTER_1: 31;

              then ((F . a1) "\/" (F . b1)) [= (F . (a1 "\/" b1)) by A6, FILTER_0: 6;

              hence thesis by A9, LATTICES: 8;

            end;

            thus (F . (a1 "/\" b1)) = ((F . a1) "/\" (F . b1))

            proof

              (a19 "/\" b19) [= b19 by LATTICES: 6;

              then [(a1 "/\" b1), b1] in R by FILTER_1: 31;

              then [(F . (a1 "/\" b1)), (F . b1)] in S by A1, WELLORD1:def 7;

              then

               A10: (F . (a19 "/\" b19)) [= (F . b19) by FILTER_1: 31;

              consider k1 be Element of L1 such that

               A11: ((F . a1) "/\" (F . b1)) = (F . k1) by A5, Th6;

              (F . k1) [= (F . b1) by A11, LATTICES: 6;

              then [(F . k1), (F . b1)] in ( LattRel L2) by FILTER_1: 31;

              then [k1, b1] in ( LattRel L1) by A1, A4, WELLORD1:def 7;

              then

               A12: k1 [= b1 by FILTER_1: 31;

              (F . k1) [= (F . a1) by A11, LATTICES: 6;

              then [(F . k1), (F . a1)] in ( LattRel L2) by FILTER_1: 31;

              then [k1, a1] in ( LattRel L1) by A1, A4, WELLORD1:def 7;

              then k1 [= a1 by FILTER_1: 31;

              then k1 [= (a1 "/\" b1) by A12, FILTER_0: 7;

              then [k1, (a1 "/\" b1)] in ( LattRel L1) by FILTER_1: 31;

              then [(F . k1), (F . (a1 "/\" b1))] in ( LattRel L2) by A1, WELLORD1:def 7;

              then

               A13: ((F . a1) "/\" (F . b1)) [= (F . (a1 "/\" b1)) by A11, FILTER_1: 31;

              (a19 "/\" b19) [= a19 by LATTICES: 6;

              then [(a1 "/\" b1), a1] in R by FILTER_1: 31;

              then [(F . (a1 "/\" b1)), (F . a1)] in S by A1, WELLORD1:def 7;

              then (F . (a19 "/\" b19)) [= (F . a19) by FILTER_1: 31;

              then (F . (a1 "/\" b1)) [= ((F . a1) "/\" (F . b1)) by A10, FILTER_0: 7;

              hence thesis by A13, LATTICES: 8;

            end;

          end;

          then F is "\/"-preserving "/\"-preserving;

          then

          reconsider F as Homomorphism of L1, L2;

          take F;

          F is one-to-one onto by A1, A3, FUNCT_2:def 3, WELLORD1:def 7;

          hence thesis;

        end;

        set R = ( LattRel L1), S = ( LattRel L2);

        given f such that

         A14: f is bijective;

        

         A15: for a,b be object 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 object;

          hereby

            assume

             A16: [a, b] in R;

            hence a in ( field R) & b in ( field R) by RELAT_1: 15;

            then

            reconsider a9 = a, b9 = b as Element of L1 by FILTER_1: 32;

            a9 [= b9 by A16, FILTER_1: 31;

            then (f . a9) [= (f . b9) by A14, Th5;

            hence [(f . a), (f . b)] in S by FILTER_1: 31;

          end;

          assume that

           A17: a in ( field R) & b in ( field R) and

           A18: [(f . a), (f . b)] in S;

          reconsider a9 = a, b9 = b as Element of L1 by A17, FILTER_1: 32;

          (f . a9) [= (f . b9) by A18, FILTER_1: 31;

          then a9 [= b9 by A14, Th5;

          hence thesis by FILTER_1: 31;

        end;

        

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

        .= ( field R) by FILTER_1: 32;

        ( rng f) = the carrier of L2 by A14, FUNCT_2:def 3

        .= ( field S) by FILTER_1: 32;

        then f is_isomorphism_of (( LattRel L1),( LattRel L2)) by A14, A19, 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;

      :: LATTICE4:def4

      pred f preserves_implication means (f . (a1 => b1)) = ((f . a1) => (f . b1));

      :: LATTICE4:def5

      pred f preserves_top means (f . ( Top L1)) = ( Top L2);

      :: LATTICE4:def6

      pred f preserves_bottom means (f . ( Bottom L1)) = ( Bottom L2);

      :: LATTICE4:def7

      pred f preserves_complement means (f . (a1 ` )) = ((f . a1) ` );

    end

    definition

      let L;

      mode ClosedSubset of L is meet-closed join-closed Subset of L;

    end

    theorem :: LATTICE4:7

    

     Th7: 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;

      

       A1: p in F & q in F implies (p "/\" q) in F;

      p in F & q in F implies (p "\/" q) in F;

      hence thesis by A1, LATTICES:def 24, LATTICES:def 25;

    end;

    registration

      let L;

      cluster non empty for ClosedSubset of L;

      existence

      proof

        the carrier of L is ClosedSubset of L by Th7;

        hence thesis;

      end;

    end

    theorem :: LATTICE4:8

    for F be Filter of L holds F is ClosedSubset of L;

    reserve B for Element of ( Fin the carrier of L);

    definition

      let L, B;

      :: LATTICE4:def8

      func FinJoin B -> Element of L equals ( FinJoin (B,( id L)));

      coherence ;

      :: LATTICE4:def9

      func FinMeet B -> Element of L equals ( FinMeet (B,( id L)));

      coherence ;

    end

    theorem :: LATTICE4:9

    

     Th9: ( FinJoin {.p.}) = p

    proof

      

      thus ( FinJoin {.p.}) = (the L_join of L $$ ( {.p.},( id L))) by LATTICE2:def 3

      .= (( id L) . p) by SETWISEO: 17

      .= p by FUNCT_1: 18;

    end;

    theorem :: LATTICE4:10

    

     Th10: ( FinMeet {.p.}) = p

    proof

      set M = the L_meet of L;

      

      thus ( FinMeet {.p.}) = (M $$ ( {.p.},( id L))) by LATTICE2:def 4

      .= (( id L) . p) by SETWISEO: 17

      .= p by FUNCT_1: 18;

    end;

    begin

    reserve DL for distributive Lattice;

    reserve f for Homomorphism of DL, L2;

    theorem :: LATTICE4:11

    

     Th11: f is onto implies L2 is distributive

    proof

      assume

       A1: f is onto;

      thus L2 is distributive

      proof

        let a,b,c be Element of L2;

        consider a9 be Element of DL such that

         A2: (f . a9) = a by A1, Th6;

        consider c9 be Element of DL such that

         A3: (f . c9) = c by A1, Th6;

        consider b9 be Element of DL such that

         A4: (f . b9) = b by A1, Th6;

        

        thus (a "/\" (b "\/" c)) = (a "/\" (f . (b9 "\/" c9))) by A4, A3, D1

        .= (f . (a9 "/\" (b9 "\/" c9))) by A2, D2

        .= (f . ((a9 "/\" b9) "\/" (a9 "/\" c9))) by LATTICES:def 11

        .= ((f . (a9 "/\" b9)) "\/" (f . (a9 "/\" c9))) by D1

        .= ((a "/\" b) "\/" (f . (a9 "/\" c9))) by A2, A4, D2

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

      end;

    end;

    begin

    reserve 0L for lower-bounded Lattice,

B,B1,B2 for Element of ( Fin the carrier of 0L),

b for Element of 0L;

    theorem :: LATTICE4:12

    

     Th12: for f be Homomorphism of 0L, L2 st f is onto holds L2 is lower-bounded & f preserves_bottom

    proof

      let f be Homomorphism of 0L, L2;

      set r = (f . ( Bottom 0L));

      assume

       A1: f is onto;

       A2:

      now

        let a2 be Element of L2;

        consider a1 be Element of 0L such that

         A3: (f . a1) = a2 by A1, Th6;

        

        thus (r "/\" a2) = (f . (( Bottom 0L) "/\" a1)) by A3, D2

        .= r;

        hence (a2 "/\" r) = r;

      end;

      thus L2 is lower-bounded by A2;

      then ( Bottom L2) = r by A2, LATTICES:def 16;

      hence thesis;

    end;

    reserve f for UnOp of the carrier of 0L;

    theorem :: LATTICE4:13

    

     Th13: ( FinJoin ((B \/ {.b.}),f)) = (( FinJoin (B,f)) "\/" (f . b))

    proof

      set J = the L_join of 0L;

      

      thus ( FinJoin ((B \/ {.b.}),f)) = (J $$ ((B \/ {.b.}),f)) by LATTICE2:def 3

      .= ((J $$ (B,f)) "\/" (f . b)) by SETWISEO: 32

      .= (( FinJoin (B,f)) "\/" (f . b)) by LATTICE2:def 3;

    end;

    theorem :: LATTICE4:14

    

     Th14: ( FinJoin (B \/ {.b.})) = (( FinJoin B) "\/" b)

    proof

      

      thus ( FinJoin (B \/ {.b.})) = (( FinJoin (B,( id 0L))) "\/" (( id 0L) . b)) by Th13

      .= (( FinJoin B) "\/" b) by FUNCT_1: 18;

    end;

    theorem :: LATTICE4:15

    (( FinJoin B1) "\/" ( FinJoin B2)) = ( FinJoin (B1 \/ B2))

    proof

      set J = the L_join of 0L;

      

      thus ( FinJoin (B1 \/ B2)) = (J $$ ((B1 \/ B2),( id 0L))) by LATTICE2:def 3

      .= ((J $$ (B1,( id 0L))) "\/" (J $$ (B2,( id 0L)))) by SETWISEO: 33

      .= (( FinJoin B1) "\/" (J $$ (B2,( id 0L)))) by LATTICE2:def 3

      .= (( FinJoin B1) "\/" ( FinJoin B2)) by LATTICE2:def 3;

    end;

    

     Lm1: for f be Function of 0L, 0L holds ( FinJoin (( {}. the carrier of 0L),f)) = ( Bottom 0L)

    proof

      let f be Function of 0L, 0L;

      set J = the L_join of 0L;

      

      thus ( FinJoin (( {}. the carrier of 0L),f)) = (J $$ (( {}. the carrier of 0L),f)) by LATTICE2:def 3

      .= ( the_unity_wrt J) by SETWISEO: 31

      .= ( Bottom 0L) by LATTICE2: 52;

    end;

    theorem :: LATTICE4:16

    ( FinJoin ( {}. the carrier of 0L)) = ( Bottom 0L) by Lm1;

    theorem :: LATTICE4:17

    

     Th17: for A be ClosedSubset of 0L st ( Bottom 0L) in A holds for B holds B c= A implies ( FinJoin B) in A

    proof

      let A be ClosedSubset of 0L;

      defpred X[ Element of ( Fin the carrier of 0L)] means $1 c= A implies ( FinJoin $1) in A;

      

       A1: for B1 be Element of ( Fin the carrier of 0L) holds for p be Element of 0L st X[B1] holds X[(B1 \/ {.p.})]

      proof

        let B1 be Element of ( Fin the carrier of 0L);

        let p be Element of 0L;

        assume

         A2: B1 c= A implies ( FinJoin B1) in A;

        assume

         A3: (B1 \/ {p}) c= A;

        then {p} c= A by XBOOLE_1: 11;

        then p in A by ZFMISC_1: 31;

        then (( FinJoin B1) "\/" p) in A by A2, A3, LATTICES:def 25, XBOOLE_1: 11;

        hence thesis by Th14;

      end;

      assume ( Bottom 0L) in A;

      then

       A4: X[( {}. the carrier of 0L)] by Lm1;

      thus for B be Element of ( Fin the carrier of 0L) holds X[B] from SETWISEO:sch 4( A4, A1);

    end;

    begin

    reserve 1L for upper-bounded Lattice,

B,B1,B2 for Element of ( Fin the carrier of 1L),

b for Element of 1L;

    theorem :: LATTICE4:18

    

     Th18: for f be Homomorphism of 1L, L2 st f is onto holds L2 is upper-bounded & f preserves_top

    proof

      let f be Homomorphism of 1L, L2;

      set r = (f . ( Top 1L));

      assume

       A1: f is onto;

       A2:

      now

        let a2 be Element of L2;

        consider a1 be Element of 1L such that

         A3: (f . a1) = a2 by A1, Th6;

        

        thus (r "\/" a2) = (f . (( Top 1L) "\/" a1)) by A3, D1

        .= r;

        hence (a2 "\/" r) = r;

      end;

      thus L2 is upper-bounded by A2;

      then ( Top L2) = r by A2, LATTICES:def 17;

      hence thesis;

    end;

    

     Lm2: for f be 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;

      

      thus ( FinMeet (( {}. the carrier of 1L),f)) = (M $$ (( {}. the carrier of 1L),f)) by LATTICE2:def 4

      .= ( the_unity_wrt M) by SETWISEO: 31

      .= ( Top 1L) by LATTICE2: 57;

    end;

    theorem :: LATTICE4:19

    ( FinMeet ( {}. the carrier of 1L)) = ( Top 1L) by Lm2;

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

    theorem :: LATTICE4:20

    

     Th20: ( FinMeet ((B \/ {.b.}),f)) = (( FinMeet (B,f)) "/\" (f . b))

    proof

      set M = the L_meet of 1L;

      

      thus ( FinMeet ((B \/ {.b.}),f)) = (M $$ ((B \/ {.b.}),f)) by LATTICE2:def 4

      .= ((M $$ (B,f)) "/\" (f . b)) by SETWISEO: 32

      .= (( FinMeet (B,f)) "/\" (f . b)) by LATTICE2:def 4;

    end;

    theorem :: LATTICE4:21

    

     Th21: ( FinMeet (B \/ {.b.})) = (( FinMeet B) "/\" b)

    proof

      

      thus ( FinMeet (B \/ {.b.})) = (( FinMeet (B,( id 1L))) "/\" (( id 1L) . b)) by Th20

      .= (( FinMeet B) "/\" b) by FUNCT_1: 18;

    end;

    theorem :: LATTICE4:22

    

     Th22: ( FinMeet ((f .: B),g)) = ( FinMeet (B,(g * f)))

    proof

      set M = the L_meet of 1L;

      

      thus ( FinMeet ((f .: B),g)) = (M $$ ((f .: B),g)) by LATTICE2:def 4

      .= (M $$ (B,(g * f))) by SETWISEO: 35

      .= ( FinMeet (B,(g * f))) by LATTICE2:def 4;

    end;

    theorem :: LATTICE4:23

    

     Th23: (( FinMeet B1) "/\" ( FinMeet B2)) = ( FinMeet (B1 \/ B2))

    proof

      set M = the L_meet of 1L;

      

      thus ( FinMeet (B1 \/ B2)) = (M $$ ((B1 \/ B2),( id 1L))) by LATTICE2:def 4

      .= ((M $$ (B1,( id 1L))) "/\" (M $$ (B2,( id 1L)))) by SETWISEO: 33

      .= (( FinMeet B1) "/\" (M $$ (B2,( id 1L)))) by LATTICE2:def 4

      .= (( FinMeet B1) "/\" ( FinMeet B2)) by LATTICE2:def 4;

    end;

    theorem :: LATTICE4:24

    

     Th24: for F be ClosedSubset of 1L st ( Top 1L) in F holds for B holds B c= F implies ( FinMeet B) in F

    proof

      let F be ClosedSubset of 1L;

      defpred X[ Element of ( Fin the carrier of 1L)] means $1 c= F implies ( FinMeet $1) in F;

      

       A1: for B1 be Element of ( Fin the carrier of 1L) holds for p be Element of 1L st X[B1] holds X[(B1 \/ {.p.})]

      proof

        let B1 be Element of ( Fin the carrier of 1L);

        let p be Element of 1L;

        assume

         A2: B1 c= F implies ( FinMeet B1) in F;

        assume

         A3: (B1 \/ {p}) c= F;

        then {p} c= F by XBOOLE_1: 11;

        then p in F by ZFMISC_1: 31;

        then (( FinMeet B1) "/\" p) in F by A2, A3, LATTICES:def 24, XBOOLE_1: 11;

        hence thesis by Th21;

      end;

      assume ( Top 1L) in F;

      then

       A4: X[( {}. the carrier of 1L)] by Lm2;

      thus for B be Element of ( Fin the carrier of 1L) holds X[B] from SETWISEO:sch 4( A4, A1);

    end;

    begin

    reserve DL for distributive upper-bounded Lattice,

B for Element of ( Fin 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;

      now

        per cases ;

          suppose B <> {} ;

          hence thesis by LATTICE2: 21, SETWISEO: 28;

        end;

          suppose

           A1: B = {} ;

           A2:

          now

            let f;

            

            thus (M $$ (B,f)) = ( FinMeet (( {}. the carrier of DL),f)) by A1, LATTICE2:def 4

            .= ( Top DL) by Lm2;

          end;

          

          hence (J . ((M $$ (B,f)),p)) = (( Top DL) "\/" p)

          .= ( Top DL)

          .= (M $$ (B,(J [:] (f,p)))) by A2;

        end;

      end;

      hence thesis;

    end;

    theorem :: LATTICE4:25

    

     Th25: (( 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 . ((M $$ (B,( id DL))),p)) by LATTICE2:def 4

      .= (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 FUNCT_2: 17

      .= ( FinMeet ((the L_join of DL [:] (( id DL),p)) .: B)) by Th22;

    end;

    begin

    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 :: LATTICE4:26

    

     Th26: ((f . i) "/\" (f . (i => j))) [= (f . j)

    proof

      (i "/\" (i => j)) [= j by FILTER_0:def 7;

      then (f . (i "/\" (i => j))) [= (f . j) by Th4;

      hence thesis by D2;

    end;

    theorem :: LATTICE4:27

    

     Th27: f is one-to-one implies (((f . i) "/\" (f . k)) [= (f . j) implies (f . k) [= (f . (i => j)))

    proof

      assume

       A1: f is one-to-one;

      hereby

        assume ((f . i) "/\" (f . k)) [= (f . j);

        then (f . (i "/\" k)) [= (f . j) by D2;

        then (i "/\" k) [= j by A1, Th5;

        then k [= (i => j) by FILTER_0:def 7;

        hence (f . k) [= (f . (i => j)) by Th4;

      end;

    end;

    theorem :: LATTICE4:28

    f is bijective implies CL is implicative & f preserves_implication

    proof

      assume

       A1: f is bijective;

      thus CL is implicative

      proof

        let p,q be Element of CL;

        consider i such that

         A2: (f . i) = p by A1, Th6;

        consider j such that

         A3: (f . j) = q by A1, Th6;

        take r = (f . (i => j));

        thus (p "/\" r) [= q by A2, A3, Th26;

        hereby

          let r1 be Element of CL;

          assume

           A4: (p "/\" r1) [= q;

          ex k st (f . k) = r1 by A1, Th6;

          hence r1 [= r by A1, A2, A3, A4, Th27;

        end;

      end;

      then

      reconsider CL as implicative Lattice;

      reconsider f as Homomorphism of IL, CL;

      now

        let i, j;

         A5:

        now

          let r1 be Element of CL;

          assume

           A6: ((f . i) "/\" r1) [= (f . j);

          ex k st (f . k) = r1 by A1, Th6;

          hence r1 [= (f . (i => j)) by A1, A6, Th27;

        end;

        ((f . i) "/\" (f . (i => j))) [= (f . j) by Th26;

        hence ((f . i) => (f . j)) = (f . (i => j)) by A5, FILTER_0:def 7;

      end;

      hence thesis;

    end;

    begin

    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,A1,A2 for Element of ( Fin the carrier of BL);

    theorem :: LATTICE4:29

    

     Th29: (( Top BL) ` ) = ( Bottom BL)

    proof

      set a = ( Bottom BL);

      

      thus (( Top BL) ` ) = ((a "\/" (a ` )) ` ) by LATTICES: 21

      .= ((a ` ) "/\" ((a ` ) ` ))

      .= ( Bottom BL);

    end;

    theorem :: LATTICE4:30

    

     Th30: (( Bottom BL) ` ) = ( Top BL)

    proof

      set a = ( Top BL);

      

      thus (( Bottom BL) ` ) = ((a "/\" (a ` )) ` ) by LATTICES: 20

      .= ((a ` ) "\/" ((a ` ) ` ))

      .= ( Top BL);

    end;

    theorem :: LATTICE4:31

    f is onto implies CL is Boolean & f preserves_complement

    proof

      assume

       A1: f is onto;

      then

       A2: f preserves_top by Th18;

      thus CL is bounded complemented;

      thus CL is distributive by A1, Th11;

      then

      reconsider CL as Boolean Lattice;

      

       A3: f preserves_bottom by A1, Th12;

      reconsider f as Homomorphism of BL, CL;

      now

        let a1;

        

         A4: ((f . (a1 ` )) "/\" (f . a1)) = (f . ((a1 ` ) "/\" a1)) by D2

        .= (f . ( Bottom BL)) by LATTICES: 20

        .= ( Bottom CL) by A3;

        

         A5: ((f . (a1 ` )) "\/" (f . a1)) = ((f . a1) "\/" (f . (a1 ` ))) & ((f . (a1 ` )) "/\" (f . a1)) = ((f . a1) "/\" (f . (a1 ` )));

        ((f . (a1 ` )) "\/" (f . a1)) = (f . ((a1 ` ) "\/" a1)) by D1

        .= (f . ( Top BL)) by LATTICES: 21

        .= ( Top CL) by A2;

        then (f . (a1 ` )) is_a_complement_of (f . a1) by A4, A5;

        hence ((f . a1) ` ) = (f . (a1 ` )) by LATTICES:def 21;

      end;

      hence thesis;

    end;

    definition

      let BL;

      :: LATTICE4:def10

      mode Field of BL -> non empty Subset of BL means

      : Def9: 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 :: LATTICE4:32

    

     Th32: 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 Def9;

      then ((a ` ) "/\" (b ` )) in F by Def9;

      then ((a "\/" b) ` ) in F by LATTICES: 24;

      then (((a "\/" b) ` ) ` ) in F by Def9;

      hence thesis;

    end;

    theorem :: LATTICE4:33

    

     Th33: a in F & b in F implies (a => b) in F

    proof

      assume that

       A1: a in F and

       A2: b in F;

      (a ` ) in F by A1, Def9;

      then ((a ` ) "\/" b) in F by A2, Th32;

      hence thesis by FILTER_0: 42;

    end;

    theorem :: LATTICE4:34

    

     Th34: 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 thesis by Def9;

    end;

    theorem :: LATTICE4:35

    

     Th35: F is ClosedSubset of BL

    proof

      

       A1: for a, b st a in F & b in F holds (a "/\" b) in F by Def9;

      for a, b st a in F & b in F holds (a "\/" b) in F by Th32;

      hence thesis by A1, LATTICES:def 24, LATTICES:def 25;

    end;

    definition

      let BL, A;

      :: LATTICE4:def11

      func field_by A -> Field of BL means

      : Def10: A c= it & for F st A c= F holds it c= F;

      existence

      proof

        set x = the Element of A;

        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 XFAMILY:sch 1;

        reconsider x as Element of BL;

        

         A2: the carrier of BL is Field of BL by Th34;

        then

         A3: X <> {} by A1;

        now

          let Z;

          assume Z in X;

          then A c= Z by A1;

          hence x in Z;

        end;

        then

        reconsider F1 = ( meet X) as non empty set by A3, SETFAM_1:def 1;

        

         A4: the carrier of BL in X by A1, A2;

        F1 c= the carrier of BL by A4, SETFAM_1:def 1;

        then

        reconsider F1 as non empty Subset of BL;

        F1 is Field of BL

        proof

          let a, b;

          assume that

           A5: a in F1 and

           A6: b in F1;

          

           A7: for Z st Z in X holds (a "/\" b) in Z

          proof

            let Z;

            assume

             A8: Z in X;

            then

             A9: b in Z by A6, SETFAM_1:def 1;

            Z is Field of BL & a in Z by A1, A5, A8, SETFAM_1:def 1;

            hence thesis by A9, Def9;

          end;

          for Z st Z in X holds (a ` ) in Z

          proof

            let Z;

            assume Z in X;

            then Z is Field of BL & a in Z by A1, A5, SETFAM_1:def 1;

            hence thesis by Def9;

          end;

          hence thesis by A3, A7, SETFAM_1:def 1;

        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: 5;

        let H;

        assume A c= H;

        then H in X by A1;

        hence thesis by SETFAM_1: 3;

      end;

      uniqueness

      proof

        let F1,F2 be Field of BL;

        assume (A c= F1 & for F st A c= F holds F1 c= F) & (A c= F2 & for F st A c= F holds F2 c= F);

        hence F1 c= F2 & F2 c= F1;

      end;

    end

    definition

      let BL, A;

      :: LATTICE4:def12

      func SetImp A -> Subset of BL equals { (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 be object;

          assume x in B;

          then ex p, q st x = (p => q) & p in A & q in A;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let BL, A;

      cluster ( SetImp A) -> non empty;

      coherence

      proof

        set x = the Element of A;

        set B = { (a => b) : a in A & b in A };

        reconsider x as Element of BL;

        (x => x) in B;

        then

        reconsider B as non empty set;

        B = ( SetImp A);

        hence thesis;

      end;

    end

    theorem :: LATTICE4:36

    x in ( SetImp A) iff ex p, q st x = (p => q) & p in A & q in A;

    theorem :: LATTICE4:37

    

     Th37: 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;

        take p, q;

        thus c = ((p ` ) "\/" q) & p in A & q in A by A1, FILTER_0: 42;

      end;

      given p, q such that

       A2: c = ((p ` ) "\/" q) and

       A3: p in A & q in A;

      c = (p => q) by A2, FILTER_0: 42;

      hence thesis by A3;

    end;

    definition

      let BL;

      deffunc U( Element of BL) = ($1 ` );

      :: LATTICE4:def13

      func comp BL -> Function of the carrier of BL, the carrier of BL means

      : Def12: (it . a) = (a ` );

      existence

      proof

        consider f be Function of the carrier of BL, the carrier of BL such that

         A1: for a holds (f . a) = U(a) from FUNCT_2:sch 4;

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        thus for f1,f2 be Function of the carrier of BL, the carrier of BL st (for x be Element of BL holds (f1 . x) = U(x)) & (for x be Element of BL holds (f2 . x) = U(x)) holds f1 = f2 from BINOP_2:sch 1;

      end;

    end

    theorem :: LATTICE4:38

    

     Th38: ( 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 Th13

      .= (( FinJoin (B,( comp BL))) "\/" (b ` )) by Def12;

    end;

    theorem :: LATTICE4:39

    (( FinJoin B) ` ) = ( FinMeet (B,( comp BL)))

    proof

      set M = the L_meet of BL;

      set J = the L_join of BL;

      

       A1: for a,b be 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))) = ((a "\/" b) ` ) by Def12

        .= ((a ` ) "/\" (b ` )) by LATTICES: 24

        .= (M . ((( comp BL) . a),(b ` ))) by Def12

        .= (M . ((( comp BL) . a),(( comp BL) . b))) by Def12;

      end;

      

       A2: (( comp BL) . ( the_unity_wrt J)) = (( the_unity_wrt J) ` ) by Def12

      .= (( Bottom BL) ` ) by LATTICE2: 52

      .= ( Top BL) by Th30

      .= ( the_unity_wrt M) by LATTICE2: 57;

      

      thus (( FinJoin B) ` ) = ((J $$ (B,( id BL))) ` ) by LATTICE2:def 3

      .= (( comp BL) . (J $$ (B,( id BL)))) by Def12

      .= (M $$ (B,(( comp BL) * ( id BL)))) by A2, A1, SETWISEO: 36

      .= (M $$ (B,( comp BL))) by FUNCT_2: 17

      .= ( FinMeet (B,( comp BL))) by LATTICE2:def 4;

    end;

    theorem :: LATTICE4:40

    ( 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 Th20

      .= (( FinMeet (B,( comp BL))) "/\" (b ` )) by Def12;

    end;

    theorem :: LATTICE4:41

    

     Th41: (( FinMeet B) ` ) = ( FinJoin (B,( comp BL)))

    proof

      set M = the L_meet of BL;

      set J = the L_join of BL;

      

       A1: for a,b be 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))) = ((a "/\" b) ` ) by Def12

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

        .= (J . ((( comp BL) . a),(b ` ))) by Def12

        .= (J . ((( comp BL) . a),(( comp BL) . b))) by Def12;

      end;

      

       A2: (( comp BL) . ( the_unity_wrt M)) = (( the_unity_wrt M) ` ) by Def12

      .= (( Top BL) ` ) by LATTICE2: 57

      .= ( Bottom BL) by Th29

      .= ( the_unity_wrt J) by LATTICE2: 52;

      

      thus (( FinMeet B) ` ) = ((M $$ (B,( id BL))) ` ) by LATTICE2:def 4

      .= (( comp BL) . (M $$ (B,( id BL)))) by Def12

      .= (J $$ (B,(( comp BL) * ( id BL)))) by A2, A1, SETWISEO: 36

      .= (J $$ (B,( comp BL))) by FUNCT_2: 17

      .= ( FinJoin (B,( comp BL))) by LATTICE2:def 3;

    end;

    theorem :: LATTICE4:42

    

     Th42: for AF be non empty ClosedSubset of BL st ( Bottom BL) in AF & ( Top BL) in AF holds 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 and

       A2: ( Top BL) in AF;

      set C = { (( FinJoin A1) "\/" ( FinJoin (A2,( comp BL)))) : A1 c= AF & A2 c= AF };

      

       A3: C c= ( SetImp AF)

      proof

        let x be object;

        assume x in C;

        then

        consider A1, A2 such that

         A4: x = (( FinJoin A1) "\/" ( FinJoin (A2,( comp BL)))) and

         A5: A1 c= AF & A2 c= AF;

        consider p, q such that

         A6: p = ( FinMeet A2) & q = ( FinJoin A1);

        

         A7: x = ((p ` ) "\/" q) by A4, A6, Th41;

        p in AF & q in AF by A1, A2, A5, A6, Th17, Th24;

        hence thesis by A7, Th37;

      end;

      defpred X[ Element of ( Fin the carrier of BL)] means $1 c= ( SetImp AF) implies ex B0 st B0 c= C & ( FinJoin ($1,( comp BL))) = ( FinMeet B0);

      let B;

      assume

       A8: B c= ( SetImp AF);

      

       A9: for B9 be Element of ( Fin the carrier of BL), b be Element of BL st X[B9] holds X[(B9 \/ {.b.})]

      proof

        set J = the L_join of BL;

        let B9 be Element of ( Fin the carrier of BL), b be Element of BL;

        assume

         A10: B9 c= ( SetImp AF) implies ex B1 st B1 c= C & ( FinJoin (B9,( comp BL))) = ( FinMeet B1);

        assume

         A11: (B9 \/ {b}) c= ( SetImp AF);

        then

        consider B1 such that

         A12: B1 c= C and

         A13: ( FinJoin (B9,( comp BL))) = ( FinMeet B1) by A10, ZFMISC_1: 137;

        b in ( SetImp AF) by A11, ZFMISC_1: 137;

        then

        consider p, q such that

         A14: b = ((p ` ) "\/" q) and

         A15: p in AF and

         A16: q in AF by Th37;

        

         A17: 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

           A18: x in ((J [:] (( id BL),b)) .: B1);

          ((J [:] (( id BL),b)) .: B1) c= the carrier of BL by FUNCT_2: 36;

          then

          reconsider x as Element of BL by A18;

          consider a such that

           A19: a in B1 and

           A20: x = ((J [:] (( id BL),b)) . a) by A18, FUNCT_2: 65;

          x = (J . ((( id BL) . a),b)) by A20, FUNCOP_1: 48

          .= (a "\/" b) by FUNCT_1: 18;

          hence thesis by A19;

        end;

        

         A21: ((J [:] (( id BL),p)) .: B1) c= C

        proof

          let x be object;

          assume x in ((J [:] (( id BL),p)) .: B1);

          then

          consider a such that

           A22: a in B1 and

           A23: x = (a "\/" p) by A17;

          a in C by A12, A22;

          then

          consider A1, A2 such that

           A24: a = (( FinJoin A1) "\/" ( FinJoin (A2,( comp BL)))) and

           A25: A1 c= AF & A2 c= AF;

          ex A19,A29 be Element of ( Fin the carrier of BL) st x = (( FinJoin A19) "\/" ( FinJoin (A29,( comp BL)))) & A19 c= AF & A29 c= AF

          proof

            take A19 = (A1 \/ {.p.});

            take A29 = A2;

            x = ((( FinJoin A1) "\/" p) "\/" ( FinJoin (A2,( comp BL)))) by A23, A24, LATTICES:def 5

            .= (( FinJoin A19) "\/" ( FinJoin (A29,( comp BL)))) by Th14;

            hence thesis by A15, A25, ZFMISC_1: 137;

          end;

          hence thesis;

        end;

        

         A26: ((J [:] (( id BL),(q ` ))) .: B1) c= C

        proof

          let x be object;

          assume x in ((J [:] (( id BL),(q ` ))) .: B1);

          then

          consider a such that

           A27: a in B1 and

           A28: x = (a "\/" (q ` )) by A17;

          a in C by A12, A27;

          then

          consider A1, A2 such that

           A29: a = (( FinJoin A1) "\/" ( FinJoin (A2,( comp BL)))) and

           A30: A1 c= AF & A2 c= AF;

          ex A19,A29 be Element of ( Fin the carrier of BL) st x = (( FinJoin A19) "\/" ( FinJoin (A29,( comp BL)))) & A19 c= AF & A29 c= AF

          proof

            take A19 = A1;

            take A29 = (A2 \/ {.q.});

            x = (( FinJoin A1) "\/" (( FinJoin (A2,( comp BL))) "\/" (q ` ))) by A28, A29, LATTICES:def 5

            .= (( FinJoin A19) "\/" ( FinJoin (A29,( comp BL)))) by Th38;

            hence thesis by A16, A30, ZFMISC_1: 137;

          end;

          hence thesis;

        end;

        take (((J [:] (( id BL),p)) .: B1) \/ ((J [:] (( id BL),(q ` ))) .: B1));

        (b ` ) = (((p ` ) ` ) "/\" (q ` )) by A14, LATTICES: 24

        .= (p "/\" (q ` ));

        

        then ( FinJoin ((B9 \/ {.b.}),( comp BL))) = (( FinMeet B1) "\/" (p "/\" (q ` ))) by A13, Th38

        .= ((( FinMeet B1) "\/" p) "/\" (( FinMeet B1) "\/" (q ` ))) by LATTICES: 11

        .= (( FinMeet ((J [:] (( id BL),p)) .: B1)) "/\" (( FinMeet B1) "\/" (q ` ))) by Th25

        .= (( FinMeet ((J [:] (( id BL),p)) .: B1)) "/\" ( FinMeet ((J [:] (( id BL),(q ` ))) .: B1))) by Th25

        .= ( FinMeet (((J [:] (( id BL),p)) .: B1) \/ ((J [:] (( id BL),(q ` ))) .: B1))) by Th23;

        hence thesis by A21, A26, XBOOLE_1: 8;

      end;

      

       A31: X[( {}. the carrier of BL)]

      proof

        assume ( {}. the carrier of BL) c= ( SetImp AF);

        take B0 = {.( Bottom BL).};

        

         A32: B0 c= C

        proof

          let x be object;

          assume x in B0;

          then

           A33: 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 A33

            .= (( Bottom BL) "\/" (( Top BL) ` )) by Th29

            .= (( FinJoin A1) "\/" (( Top BL) ` )) by Th9

            .= (( FinJoin A1) "\/" (( FinMeet A2) ` )) by Th10

            .= (( FinJoin A1) "\/" ( FinJoin (A2,( comp BL)))) by Th41;

            thus A1 c= AF by A1, ZFMISC_1: 31;

            thus thesis by A2, ZFMISC_1: 31;

          end;

          hence thesis;

        end;

        ( FinJoin (( {}. the carrier of BL),( comp BL))) = ( Bottom BL) by Lm1

        .= ( FinMeet {.( Bottom BL).}) by Th10;

        hence thesis by A32;

      end;

      for B be Element of ( Fin the carrier of BL) holds X[B] from SETWISEO:sch 4( A31, A9);

      then ex B1 st B1 c= C & ( FinJoin (B,( comp BL))) = ( FinMeet B1) by A8;

      hence thesis by A3, XBOOLE_1: 1;

    end;

    theorem :: LATTICE4:43

    for AF be 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 and

       A2: ( Top BL) in AF;

      set A1 = { ( FinMeet B) : B c= ( SetImp AF) };

      

       A3: AF c= A1

      proof

        let x be object;

        assume

         A4: x in AF;

        then

        reconsider b = x as Element of BL;

        reconsider B = {.b.} as Element of ( Fin the carrier of BL);

        b = (( Bottom BL) "\/" b)

        .= ((( Top BL) ` ) "\/" b) by Th29;

        then b in ( SetImp AF) by A2, A4, Th37;

        then

         A5: B c= ( SetImp AF) by ZFMISC_1: 31;

        x = ( FinMeet B) by Th10;

        hence thesis by A5;

      end;

      A1 c= the carrier of BL

      proof

        let x be object;

        assume x in A1;

        then ex B st x = ( FinMeet B) & B c= ( SetImp AF);

        hence thesis;

      end;

      then

      reconsider A1 as non empty Subset of BL by A3;

       A6:

      now

        let F;

        assume

         A7: AF c= F;

        thus A1 c= F

        proof

          reconsider F1 = F as ClosedSubset of BL by Th35;

          let x be object;

          assume x in A1;

          then

          consider B such that

           A8: x = ( FinMeet B) and

           A9: B c= ( SetImp AF);

          ( SetImp AF) c= F

          proof

            let y be object;

            assume y in ( SetImp AF);

            then ex p, q st y = (p => q) & p in AF & q in AF;

            hence thesis by A7, Th33;

          end;

          then B c= F1 by A9;

          hence thesis by A2, A7, A8, Th24;

        end;

      end;

      A1 is Field of BL

      proof

        let p, q;

        assume that

         A10: p in A1 and

         A11: q in A1;

        thus (p "/\" q) in A1

        proof

          consider B2 such that

           A12: q = ( FinMeet B2) & B2 c= ( SetImp AF) by A11;

          consider B1 such that

           A13: p = ( FinMeet B1) & B1 c= ( SetImp AF) by A10;

          consider B0 such that

           A14: B0 = (B1 \/ B2);

          B0 c= ( SetImp AF) & (p "/\" q) = ( FinMeet B0) by A13, A12, A14, Th23, XBOOLE_1: 8;

          hence thesis;

        end;

        thus (p ` ) in A1

        proof

          consider B such that

           A15: p = ( FinMeet B) and

           A16: B c= ( SetImp AF) by A10;

          (p ` ) = ( FinJoin (B,( comp BL))) by A15, Th41;

          then ex B0 st B0 c= ( SetImp AF) & (p ` ) = ( FinMeet B0) by A1, A2, A16, Th42;

          hence thesis;

        end;

      end;

      hence thesis by A3, A6, Def10;

    end;