latstone.miz



    begin

    theorem :: LATSTONE:1

    

     ThA: for L be distributive Lattice, S be Sublattice of L holds S is distributive

    proof

      let L be distributive Lattice, S be Sublattice of L;

      let a,b,c be Element of S;

      reconsider aa = a, bb = b, cc = c as Element of L by FILTER_2: 68;

      

       A2: (b "\/" c) = (bb "\/" cc) by MSUALG_7: 11;

      reconsider ab = (aa "/\" bb), ac = (aa "/\" cc) as Element of L;

      

       A4: ab = (a "/\" b) & ac = (a "/\" c) by MSUALG_7: 11;

      (a "/\" (b "\/" c)) = (aa "/\" (bb "\/" cc)) by MSUALG_7: 11, A2

      .= ((aa "/\" bb) "\/" (aa "/\" cc)) by LATTICES:def 11

      .= ((a "/\" b) "\/" (a "/\" c)) by MSUALG_7: 11, A4;

      hence thesis;

    end;

    registration

      let L be distributive Lattice;

      cluster -> distributive for Sublattice of L;

      coherence by ThA;

    end

    registration

      let L1,L2 be bounded Lattice;

      cluster [:L1, L2:] -> bounded;

      coherence by FILTER_1: 41;

    end

    reserve L for Lattice;

    reserve I,P for non empty ClosedSubset of L;

    theorem :: LATSTONE:2

    

     ThB: L is lower-bounded & ( Bottom L) in I implies ( latt (L,I)) is lower-bounded & ( Bottom ( latt (L,I))) = ( Bottom L)

    proof

      set b9 = the Element of ( latt (L,I));

      reconsider b = b9 as Element of L by FILTER_2: 68;

      assume

       A0: L is lower-bounded & ( Bottom L) in I;

      set c = ( Bottom L);

      reconsider c9 = c as Element of ( latt (L,I)) by FILTER_2: 72, A0;

      ex c9 be Element of ( latt (L,I)) st for a9 be Element of ( latt (L,I)) holds (c9 "/\" a9) = c9 & (a9 "/\" c9) = c9

      proof

        take c9;

        let a9 be Element of ( latt (L,I));

        reconsider a = a9 as Element of L by FILTER_2: 68;

        

        thus (c9 "/\" a9) = (c "/\" a) by FILTER_2: 73

        .= c9 by A0;

        hence thesis;

      end;

      hence

       W1: ( latt (L,I)) is lower-bounded by LATTICES:def 13;

      for a9 be Element of ( latt (L,I)) holds (c9 "/\" a9) = c9 & (a9 "/\" c9) = c9

      proof

        let a9 be Element of ( latt (L,I));

        reconsider a = a9 as Element of L by FILTER_2: 68;

        

        thus (c9 "/\" a9) = (c "/\" a) by FILTER_2: 73

        .= c9 by A0;

        hence thesis;

      end;

      hence thesis by LATTICES:def 16, W1;

    end;

    theorem :: LATSTONE:3

    

     ThC: L is upper-bounded & ( Top L) in I implies ( latt (L,I)) is upper-bounded & ( Top ( latt (L,I))) = ( Top L)

    proof

      set b9 = the Element of ( latt (L,I));

      reconsider b = b9 as Element of L by FILTER_2: 68;

      assume

       A0: L is upper-bounded & ( Top L) in I;

      set c = ( Top L);

      reconsider c9 = c as Element of ( latt (L,I)) by FILTER_2: 72, A0;

      ex c9 be Element of ( latt (L,I)) st for a9 be Element of ( latt (L,I)) holds (c9 "\/" a9) = c9 & (a9 "\/" c9) = c9

      proof

        take c9;

        let a9 be Element of ( latt (L,I));

        reconsider a = a9 as Element of L by FILTER_2: 68;

        

        thus (c9 "\/" a9) = (c "\/" a) by FILTER_2: 73

        .= c9 by A0;

        hence thesis;

      end;

      hence

       W1: ( latt (L,I)) is upper-bounded by LATTICES:def 14;

      for a9 be Element of ( latt (L,I)) holds (c9 "\/" a9) = c9 & (a9 "\/" c9) = c9

      proof

        let a9 be Element of ( latt (L,I));

        reconsider a = a9 as Element of L by FILTER_2: 68;

        

        thus (c9 "\/" a9) = (c "\/" a) by FILTER_2: 73

        .= c9 by A0;

        hence thesis;

      end;

      hence thesis by LATTICES:def 17, W1;

    end;

    begin

    ::$Notion-Name

    definition

      let L be non empty LattStr;

      let a,b be Element of L;

      :: LATSTONE:def1

      pred a is_a_pseudocomplement_of b means (a "/\" b) = ( Bottom L) & for x be Element of L st (b "/\" x) = ( Bottom L) holds x [= a;

    end

    definition

      let L be non empty LattStr;

      :: LATSTONE:def2

      attr L is pseudocomplemented means

      : def2: for x be Element of L holds ex y be Element of L st y is_a_pseudocomplement_of x;

    end

    theorem :: LATSTONE:4

    

     Th1: for L be Boolean Lattice holds L is pseudocomplemented

    proof

      let L be Boolean Lattice;

      L is pseudocomplemented

      proof

        let x be Element of L;

        take y = (x ` );

        for z be Element of L st (x "/\" z) = ( Bottom L) holds z [= y

        proof

          let z be Element of L;

          assume

           E1: (x "/\" z) = ( Bottom L);

          z = (z "/\" ( Top L))

          .= (z "/\" (x "\/" y)) by LATTICES: 21

          .= ((z "/\" x) "\/" (z "/\" y)) by LATTICES:def 11

          .= (z "/\" y) by E1;

          hence z [= y by LATTICES: 4;

        end;

        hence thesis by LATTICES: 20;

      end;

      hence thesis;

    end;

    registration

      cluster Boolean -> pseudocomplemented for Lattice;

      coherence by Th1;

    end

    registration

      cluster Boolean pseudocomplemented bounded for Lattice;

      existence

      proof

        set L = the Boolean Lattice;

        take L;

        thus thesis;

      end;

    end

    theorem :: LATSTONE:5

    

     Th2: for L be pseudocomplemented lower-bounded Lattice, a,b,x be Element of L st a is_a_pseudocomplement_of x & b is_a_pseudocomplement_of x holds a = b

    proof

      let L be pseudocomplemented lower-bounded Lattice;

      let a,b,x be Element of L;

      assume that

       a1: a is_a_pseudocomplement_of x and

       b1: b is_a_pseudocomplement_of x;

      

       a2: (a "/\" x) = ( Bottom L) by a1;

      

       b2: (b "/\" x) = ( Bottom L) by b1;

      

       ab1: b [= a by a1, b2;

      a [= b by b1, a2;

      hence a = b by ab1, LATTICES: 8;

    end;

    definition

      let L be non empty LattStr, x be Element of L;

      assume

       A1: L is pseudocomplemented lower-bounded Lattice;

      :: LATSTONE:def3

      func x * -> Element of L means

      : def3: it is_a_pseudocomplement_of x;

      existence by def2, A1;

      uniqueness by A1, Th2;

    end

    theorem :: LATSTONE:6

    

     ThD: for L be pseudocomplemented lower-bounded Lattice, x be Element of L holds ((x * ) "/\" x) = ( Bottom L)

    proof

      let L be pseudocomplemented lower-bounded Lattice, x be Element of L;

      (x * ) is_a_pseudocomplement_of x by def3;

      hence thesis;

    end;

    reserve L for lower-bounded pseudocomplemented Lattice;

    theorem :: LATSTONE:7

    

     Th5: for a be Element of L holds a [= ((a * ) * )

    proof

      let a be Element of L;

      

       a1: ((a * ) * ) is_a_pseudocomplement_of (a * ) by def3;

      (a * ) is_a_pseudocomplement_of a by def3;

      hence thesis by a1;

    end;

    theorem :: LATSTONE:8

    

     Th6: for a,b be Element of L holds a [= b implies (b * ) [= (a * )

    proof

      let a,b be Element of L;

      assume a [= b;

      then

       a1: (a "/\" b) = a by LATTICES: 4;

      

       a2: (a * ) is_a_pseudocomplement_of a by def3;

      (a "/\" (b * )) = (((b * ) "/\" b) "/\" a) by a1, LATTICES:def 7

      .= (( Bottom L) "/\" a) by ThD

      .= ( Bottom L);

      hence (b * ) [= (a * ) by a2;

    end;

    theorem :: LATSTONE:9

    

     Th7: for a be Element of L holds (a * ) = (((a * ) * ) * )

    proof

      let a be Element of L;

      

       a1: (((a * ) * ) * ) [= (a * ) by Th6, Th5;

      (a * ) [= (((a * ) * ) * ) by Th5;

      hence thesis by a1, LATTICES: 8;

    end;

    theorem :: LATSTONE:10

    

     Th11: for L be pseudocomplemented bounded Lattice holds (( Bottom L) * ) = ( Top L)

    proof

      let L be pseudocomplemented bounded Lattice;

      ( Top L) is_a_pseudocomplement_of ( Bottom L) by LATTICES: 19;

      hence (( Bottom L) * ) = ( Top L) by def3;

    end;

    theorem :: LATSTONE:11

    

     Th11a: for L be pseudocomplemented bounded Lattice holds (( Top L) * ) = ( Bottom L)

    proof

      let L be pseudocomplemented bounded Lattice;

      for x be Element of L st (( Top L) "/\" x) = ( Bottom L) holds x [= ( Bottom L);

      then ( Bottom L) is_a_pseudocomplement_of ( Top L);

      hence (( Top L) * ) = ( Bottom L) by def3;

    end;

    theorem :: LATSTONE:12

    

     ThE: for L be Boolean Lattice, x be Element of L holds (x ` ) = (x * )

    proof

      let L be Boolean Lattice, x be Element of L;

      

       a1: (x * ) [= (x ` )

      proof

        ((x * ) "/\" x) = ( Bottom L) by ThD;

        hence thesis by LATTICES: 25;

      end;

      (x ` ) [= (x * )

      proof

        

         a1: ((x ` ) "/\" x) = ( Bottom L) by LATTICES: 20;

        (x * ) is_a_pseudocomplement_of x by def3;

        hence thesis by a1;

      end;

      hence thesis by a1, LATTICES: 8;

    end;

    theorem :: LATSTONE:13

    

     ThF: for L be pseudocomplemented bounded Lattice, x,y be Element of L st y is_a_pseudocomplement_of x holds y in ( PseudoComplements x)

    proof

      let L be pseudocomplemented bounded Lattice, x,y be Element of L;

      assume y is_a_pseudocomplement_of x;

      then (x "/\" y) = ( Bottom L);

      then y in { xx where xx be Element of L : (x "/\" xx) = ( Bottom L) };

      hence thesis by LATTICEA:def 8;

    end;

    theorem :: LATSTONE:14

    for L be pseudocomplemented bounded Lattice, x be Element of L holds (x * ) in ( PseudoComplements x)

    proof

      let L be pseudocomplemented bounded Lattice, a be Element of L;

      (a * ) is_a_pseudocomplement_of a by def3;

      hence thesis by ThF;

    end;

    begin

    definition

      let L be lower-bounded pseudocomplemented Lattice;

      :: LATSTONE:def4

      func Skeleton L -> Subset of L equals the set of all (a * ) where a be Element of L;

      coherence

      proof

        { (a * ) where a be Element of L : not contradiction } c= the carrier of L

        proof

          let x be object;

          assume x in { (a * ) where a be Element of L : not contradiction };

          then

          consider a be Element of L such that

           A1: x = (a * );

          thus thesis by A1;

        end;

        hence thesis;

      end;

    end

    theorem :: LATSTONE:15

    for L be lower-bounded pseudocomplemented Lattice holds ( Skeleton L) = { a where a be Element of L : ((a * ) * ) = a }

    proof

      let L be lower-bounded pseudocomplemented Lattice;

      thus ( Skeleton L) c= { a where a be Element of L : ((a * ) * ) = a }

      proof

        let x be object;

        assume x in ( Skeleton L);

        then

        consider a be Element of L such that

         a1: x = (a * );

        (((a * ) * ) * ) = (a * ) by Th7;

        hence thesis by a1;

      end;

      let x be object;

      assume x in { a where a be Element of L : ((a * ) * ) = a };

      then

      consider a be Element of L such that

       a3: x = a & ((a * ) * ) = a;

      thus thesis by a3;

    end;

    theorem :: LATSTONE:16

    

     Th13: for L be lower-bounded pseudocomplemented Lattice, x be Element of L holds x in ( Skeleton L) iff ((x * ) * ) = x

    proof

      let L be lower-bounded pseudocomplemented Lattice, x be Element of L;

      hereby

        assume x in ( Skeleton L);

        then

        consider a be Element of L such that

         a1: x = (a * );

        thus ((x * ) * ) = x by a1, Th7;

      end;

      assume ((x * ) * ) = x;

      hence x in ( Skeleton L);

    end;

    registration

      let L be bounded pseudocomplemented Lattice;

      cluster ( Skeleton L) -> non empty;

      coherence

      proof

        set x = the Element of L;

        (x * ) in ( Skeleton L);

        hence thesis;

      end;

    end

    theorem :: LATSTONE:17

    for L be pseudocomplemented distributive lower-bounded Lattice holds for a,b be Element of L st a in ( Skeleton L) & b in ( Skeleton L) holds (a "/\" b) in ( Skeleton L)

    proof

      let L be pseudocomplemented distributive lower-bounded Lattice;

      let a,b be Element of L;

      assume a in ( Skeleton L) & b in ( Skeleton L);

      then

       A2: a = ((a * ) * ) & b = ((b * ) * ) by Th13;

      (a * ) [= ((a "/\" b) * ) by Th6, LATTICES: 6;

      then

       B2: (((a "/\" b) * ) * ) [= a by A2, Th6;

      (b * ) [= ((a "/\" b) * ) by Th6, LATTICES: 6;

      then (((a "/\" b) * ) * ) [= ((b * ) * ) by Th6;

      then

       B1: (((a "/\" b) * ) * ) [= (a "/\" b) by B2, FILTER_0: 7, A2;

      (a "/\" b) [= (((a "/\" b) * ) * ) by Th5;

      then (a "/\" b) = (((a "/\" b) * ) * ) by B1, LATTICES: 8;

      hence thesis;

    end;

    begin

    definition

      let L be non empty LattStr;

      :: LATSTONE:def5

      attr L is satisfying_Stone_identity means

      : SatStone: for x be Element of L holds ((x * ) "\/" ((x * ) * )) = ( Top L);

    end

    theorem :: LATSTONE:18

    

     Th4: for L be Boolean Lattice holds L is satisfying_Stone_identity

    proof

      let L be Boolean Lattice, x be Element of L;

      ((x * ) "\/" ((x * ) * )) = ( Top L)

      proof

        ((x * ) "\/" ((x * ) * )) = ((x ` ) "\/" ((x * ) * )) by ThE

        .= ((x ` ) "\/" ((x ` ) * )) by ThE

        .= ((x ` ) "\/" ((x ` ) ` )) by ThE

        .= ( Top L) by LATTICES: 21;

        hence thesis;

      end;

      hence thesis;

    end;

    registration

      cluster Boolean -> satisfying_Stone_identity for Lattice;

      coherence by Th4;

    end

    registration

      cluster satisfying_Stone_identity pseudocomplemented Boolean for Lattice;

      existence

      proof

        set L = the Boolean Lattice;

        take L;

        thus thesis;

      end;

    end

    theorem :: LATSTONE:19

    

     Th12: for L be pseudocomplemented distributive bounded Lattice holds L is satisfying_Stone_identity iff for a,b be Element of L holds ((a "/\" b) * ) = ((a * ) "\/" (b * ))

    proof

      let L be pseudocomplemented distributive bounded Lattice;

      hereby

        assume

         a11: L is satisfying_Stone_identity;

        let a,b be Element of L;

        set g = (a "/\" b);

        

         a0: (g "/\" ((a * ) "\/" (b * ))) = (((a * ) "/\" g) "\/" (g "/\" (b * ))) by LATTICES:def 11

        .= ((((a * ) "/\" a) "/\" b) "\/" (g "/\" (b * ))) by LATTICES:def 7

        .= ((((a * ) "/\" a) "/\" b) "\/" (a "/\" (b "/\" (b * )))) by LATTICES:def 7

        .= ((( Bottom L) "/\" b) "\/" (a "/\" (b "/\" (b * )))) by ThD

        .= ((( Bottom L) "/\" b) "\/" (a "/\" ( Bottom L))) by ThD

        .= ( Bottom L);

        for x be Element of L st (g "/\" x) = ( Bottom L) holds x [= ((a * ) "\/" (b * ))

        proof

          let x be Element of L;

          set z = (b "/\" x);

          set w = (x "/\" ((a * ) * ));

          assume

           a1: (g "/\" x) = ( Bottom L);

          

           a0: ( Bottom L) [= ((b "/\" x) "/\" ((a * ) * )) by LATTICES: 16;

          

           a2: ((b "/\" x) "/\" a) = ( Bottom L) by a1, LATTICES:def 7;

          (a * ) is_a_pseudocomplement_of a by def3;

          then ((b "/\" x) "/\" ((a * ) * )) [= ((a * ) "/\" ((a * ) * )) by LATTICES: 9, a2;

          then ((b "/\" x) "/\" ((a * ) * )) [= ( Bottom L) by ThD;

          then ((b "/\" x) "/\" ((a * ) * )) = ( Bottom L) by LATTICES: 8, a0;

          then

           a4: ((x "/\" ((a * ) * )) "/\" b) = ( Bottom L) by LATTICES:def 7;

          (b * ) is_a_pseudocomplement_of b by def3;

          then

           a5: (x "/\" ((a * ) * )) [= (b * ) by a4;

          

           a6: (x "/\" (a * )) [= (a * ) by LATTICES: 6;

          x = (x "/\" ( Top L))

          .= (x "/\" ((a * ) "\/" ((a * ) * ))) by a11

          .= ((x "/\" (a * )) "\/" (x "/\" ((a * ) * ))) by LATTICES:def 11;

          hence x [= ((a * ) "\/" (b * )) by a5, a6, FILTER_0: 4;

        end;

        then ((a * ) "\/" (b * )) is_a_pseudocomplement_of (a "/\" b) by a0;

        hence ((a "/\" b) * ) = ((a * ) "\/" (b * )) by def3;

      end;

      assume

       a1: for a,b be Element of L holds ((a "/\" b) * ) = ((a * ) "\/" (b * ));

      let x be Element of L;

      (x "/\" (x * )) = ( Bottom L) by ThD;

      then ((x * ) "\/" ((x * ) * )) = (( Bottom L) * ) by a1;

      hence thesis by Th11;

    end;

    ::$Notion-Name

    definition

      let L be Lattice;

      :: LATSTONE:def6

      attr L is Stone means L is pseudocomplemented distributive bounded satisfying_Stone_identity;

    end

    registration

      cluster Stone -> pseudocomplemented distributive bounded satisfying_Stone_identity for Lattice;

      coherence ;

      cluster pseudocomplemented distributive bounded satisfying_Stone_identity -> Stone for Lattice;

      coherence ;

    end

    theorem :: LATSTONE:20

    for L be pseudocomplemented distributive bounded Lattice holds L is satisfying_Stone_identity iff for a,b be Element of L st a in ( Skeleton L) & b in ( Skeleton L) holds (a "\/" b) in ( Skeleton L)

    proof

      let L be pseudocomplemented distributive bounded Lattice;

      hereby

        assume

         a0: L is satisfying_Stone_identity;

        let a,b be Element of L;

        assume

         X0: a in ( Skeleton L) & b in ( Skeleton L);

        then

        consider x be Element of L such that

         X1: a = (x * );

        consider y be Element of L such that

         X2: b = (y * ) by X0;

        ((x "/\" y) * ) in ( Skeleton L);

        hence (a "\/" b) in ( Skeleton L) by X1, X2, Th12, a0;

      end;

      assume

       a1: for a,b be Element of L st a in ( Skeleton L) & b in ( Skeleton L) holds (a "\/" b) in ( Skeleton L);

      let y be Element of L;

      (y * ) in ( Skeleton L) & ((y * ) * ) in ( Skeleton L);

      then

       sp: ((((y * ) "\/" ((y * ) * )) * ) * ) = ((y * ) "\/" ((y * ) * )) by Th13, a1;

      

       r1: ((y * ) * ) [= (((y * ) "/\" ((y * ) * )) * ) by Th6, LATTICES: 6;

      (((y * ) * ) * ) [= (((y * ) "/\" ((y * ) * )) * ) by LATTICES: 6, Th6;

      then (y * ) [= (((y * ) "/\" ((y * ) * )) * ) by Th7;

      then

       r: ((y * ) "\/" ((y * ) * )) [= ((((y * ) "/\" ((y * ) * )) * ) "\/" (((y * ) "/\" ((y * ) * )) * )) by r1, FILTER_0: 4;

      

       s1: (((y * ) "\/" ((y * ) * )) * ) [= ((y * ) * ) by Th6, LATTICES: 5;

      (((y * ) "\/" ((y * ) * )) * ) [= (((y * ) * ) * ) by Th6, LATTICES: 5;

      then

       s2: (((y * ) "\/" ((y * ) * )) * ) [= (y * ) by Th7;

      ((((y * ) "\/" ((y * ) * )) * ) "/\" (((y * ) "\/" ((y * ) * )) * )) [= ((y * ) "/\" ((y * ) * )) by s1, s2, FILTER_0: 5;

      then (((y * ) "/\" ((y * ) * )) * ) [= ((y * ) "\/" ((y * ) * )) by sp, Th6;

      then (((y * ) "/\" ((y * ) * )) * ) = ((y * ) "\/" ((y * ) * )) by r, LATTICES: 8;

      then (( Bottom L) * ) = ((y * ) "\/" ((y * ) * )) by ThD;

      hence thesis by Th11;

    end;

    reserve L for Stone Lattice;

    theorem :: LATSTONE:21

    

     Lm1: ( Top L) in ( Skeleton L) & ( Bottom L) in ( Skeleton L)

    proof

      (( Top L) * ) in ( Skeleton L) & (( Bottom L) * ) in ( Skeleton L);

      hence thesis by Th11a, Th11;

    end;

    definition

      let L be Stone Lattice, a be Element of L;

      :: LATSTONE:def7

      attr a is skeletal means a in ( Skeleton L);

    end

    registration

      let L be Stone Lattice;

      cluster ( Top L) -> skeletal;

      coherence by Lm1;

      cluster ( Bottom L) -> skeletal;

      coherence by Lm1;

    end

    registration

      let L be Stone Lattice;

      cluster ( Skeleton L) -> join-closed meet-closed;

      coherence

      proof

        set S = ( Skeleton L);

        

         tt: for p,q be Element of L st p in S & q in S holds (p "\/" q) in S

        proof

          let p,q be Element of L;

          assume p in S & q in S;

          then ((p * ) * ) = p & ((q * ) * ) = q by Th13;

          then (p "\/" q) = (((p * ) "/\" (q * )) * ) by Th12;

          hence thesis;

        end;

        for p,q be Element of L st p in S & q in S holds (p "/\" q) in S

        proof

          let p,q be Element of L;

          assume

           T1: p in S & q in S;

          then

           T3: p = ((p * ) * ) by Th13;

          (p * ) [= ((p "/\" q) * ) by Th6, LATTICES: 6;

          then

           T2: (((p "/\" q) * ) * ) [= ((p * ) * ) by Th6;

          

           T4: q = ((q * ) * ) by T1, Th13;

          (q * ) [= ((p "/\" q) * ) by Th6, LATTICES: 6;

          then (((p "/\" q) * ) * ) [= ((q * ) * ) by Th6;

          then

           T5: (((p "/\" q) * ) * ) [= (p "/\" q) by T3, T4, T2, FILTER_0: 7;

          (p "/\" q) [= (((p "/\" q) * ) * ) by Th5;

          then (p "/\" q) = (((p "/\" q) * ) * ) by T5, LATTICES: 8;

          hence thesis;

        end;

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

      end;

    end

    definition

      let L be Stone Lattice;

      :: original: Skeleton

      redefine

      func Skeleton L -> ClosedSubset of L ;

      coherence ;

    end

    definition

      let L be Stone Lattice;

      :: LATSTONE:def8

      func SkelLatt L -> Sublattice of L equals ( latt (L,( Skeleton L)));

      coherence ;

    end

    registration

      let L be Stone Lattice;

      cluster ( SkelLatt L) -> distributive;

      coherence ;

    end

    theorem :: LATSTONE:22

    ( Bottom L) = ( Bottom ( SkelLatt L)) & ( Top L) = ( Top ( SkelLatt L))

    proof

      ( Bottom L) in ( Skeleton L) & ( Top L) in ( Skeleton L) by Lm1;

      hence thesis by ThB, ThC;

    end;

    

     LattIsComplemented: ( latt (L,( Skeleton L))) is complemented

    proof

      set P = ( Skeleton L);

      

       A0: ( Bottom L) in P & ( Top L) in P by Lm1;

      set LL = ( latt (L,P));

      for b be Element of LL holds ex a be Element of LL st a is_a_complement_of b

      proof

        let b be Element of LL;

        reconsider bb = b as Element of L by FILTER_2: 68;

        set aa = (bb * );

        (bb * ) in ( Skeleton L);

        then

        reconsider a = aa as Element of LL by FILTER_2: 72;

        b in the carrier of LL;

        then

         z1: b in ( Skeleton L) by FILTER_2: 72;

        (aa "\/" bb) = ((((bb * ) * ) * ) "\/" bb) by z1, Th13

        .= ((((bb * ) * ) * ) "\/" ((bb * ) * )) by z1, Th13

        .= ( Top L) by SatStone;

        

        then

         A1: (a "\/" b) = ( Top L) by FILTER_2: 73

        .= ( Top LL) by A0, ThC;

        (aa "/\" bb) = ( Bottom L) by ThD;

        

        then (a "/\" b) = ( Bottom L) by FILTER_2: 73

        .= ( Bottom LL) by A0, ThB;

        hence thesis by LATTICES:def 18, A1;

      end;

      hence thesis by LATTICES:def 19;

    end;

    registration

      let L be Stone Lattice;

      cluster ( SkelLatt L) -> Boolean;

      coherence

      proof

        ( Top L) in ( Skeleton L) by Lm1;

        then

         A0: ( latt (L,( Skeleton L))) is upper-bounded by ThC;

        ( Bottom L) in ( Skeleton L) by Lm1;

        then

         a2: ( latt (L,( Skeleton L))) is lower-bounded by ThB;

        ( latt (L,( Skeleton L))) is complemented by LattIsComplemented;

        hence thesis by a2, A0;

      end;

    end

    begin

    definition

      let L be lower-bounded Lattice;

      :: LATSTONE:def9

      func DenseElements L -> Subset of L equals { a where a be Element of L : (a * ) = ( Bottom L) };

      coherence

      proof

        { a where a be Element of L : (a * ) = ( Bottom L) } c= the carrier of L

        proof

          let x be object;

          assume x in { a where a be Element of L : (a * ) = ( Bottom L) };

          then

          consider aa be Element of L such that

           A1: aa = x & (aa * ) = ( Bottom L);

          thus thesis by A1;

        end;

        hence thesis;

      end;

    end

    theorem :: LATSTONE:23

    

     TopIsDense: ( Top L) in ( DenseElements L)

    proof

      (( Top L) * ) = ( Bottom L) by Th11a;

      hence thesis;

    end;

    registration

      let L be Stone Lattice;

      cluster ( DenseElements L) -> non empty;

      coherence by TopIsDense;

    end

    definition

      let L be Stone Lattice, a be Element of L;

      :: LATSTONE:def10

      attr a is dense means a in ( DenseElements L);

    end

    registration

      let L be Stone Lattice;

      cluster ( Top L) -> dense;

      coherence by TopIsDense;

    end

    theorem :: LATSTONE:24

    

     DenseIsBot: for L be Stone Lattice, x be Element of L st x in ( DenseElements L) holds (x * ) = ( Bottom L)

    proof

      let L be Stone Lattice, x be Element of L;

      assume x in ( DenseElements L);

      then

      consider aa be Element of L such that

       A1: x = aa & (aa * ) = ( Bottom L);

      thus thesis by A1;

    end;

    registration

      let L be Stone Lattice;

      cluster ( DenseElements L) -> join-closed meet-closed;

      coherence

      proof

        

         A1: for x,y be Element of L st x in ( DenseElements L) & y in ( DenseElements L) holds (x "\/" y) in ( DenseElements L)

        proof

          let x,y be Element of L;

          assume x in ( DenseElements L) & y in ( DenseElements L);

          then

           A2: (x * ) = ( Bottom L) & (y * ) = ( Bottom L) by DenseIsBot;

          

           F1: ((x "\/" y) * ) [= (x * ) by Th6, LATTICES: 5;

          ( Bottom L) [= ((x "\/" y) * ) by LATTICES: 16;

          then ((x "\/" y) * ) = ( Bottom L) by LATTICES: 8, A2, F1;

          hence (x "\/" y) in ( DenseElements L);

        end;

        for x,y be Element of L st x in ( DenseElements L) & y in ( DenseElements L) holds (x "/\" y) in ( DenseElements L)

        proof

          let x,y be Element of L;

          assume x in ( DenseElements L) & y in ( DenseElements L);

          then

           A2: (x * ) = ( Bottom L) & (y * ) = ( Bottom L) by DenseIsBot;

          ((x "/\" y) * ) = ((x * ) "\/" (y * )) by Th12;

          hence (x "/\" y) in ( DenseElements L) by A2;

        end;

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

      end;

    end

    definition

      let L be Stone Lattice;

      :: original: DenseElements

      redefine

      func DenseElements L -> ClosedSubset of L ;

      coherence ;

    end

    definition

      let L be Stone Lattice;

      :: LATSTONE:def11

      func DenseLatt L -> Sublattice of L equals ( latt (L,( DenseElements L)));

      coherence ;

    end

    registration

      let L be Stone Lattice;

      cluster ( DenseLatt L) -> distributive;

      coherence ;

    end

    theorem :: LATSTONE:25

    for L be Stone Lattice, a be Element of L holds ex b,c be Element of L st a = (b "/\" c) & b in ( Skeleton L) & c in ( DenseElements L)

    proof

      let L be Stone Lattice, a be Element of L;

      

       A1: a = ((((a * ) * ) "/\" a) "\/" ( Bottom L)) by LATTICES: 4, Th5

      .= ((((a * ) * ) "/\" a) "\/" (((a * ) * ) "/\" (a * ))) by ThD

      .= (((a * ) * ) "/\" (a "\/" (a * ))) by LATTICES:def 11;

      take b = ((a * ) * );

      take c = (a "\/" (a * ));

      

       G1: ((a "\/" (a * )) * ) [= (a * ) by Th6, LATTICES: 5;

      ((a "\/" (a * )) * ) [= ((a * ) * ) by Th6, LATTICES: 5;

      then ((a "\/" (a * )) * ) [= ((a * ) "/\" ((a * ) * )) by FILTER_0: 7, G1;

      then ((a "\/" (a * )) * ) [= ( Bottom L) by ThD;

      then ((a "\/" (a * )) * ) = ( Bottom L) by BOOLEALG: 9;

      hence thesis by A1;

    end;

    begin

    theorem :: LATSTONE:26

    for p be Prime holds ( NatDivisors p) = {1, p}

    proof

      let p be Prime;

      

       a1: ( NatDivisors (p |^ 1)) = { (p |^ k) where k be Element of NAT : k <= 1 } by NAT_5: 19;

      { (p |^ k) where k be Element of NAT : k <= 1 } = {1, p}

      proof

        thus { (p |^ k) where k be Element of NAT : k <= 1 } c= {1, p}

        proof

          let x be object;

          assume x in { (p |^ k) where k be Element of NAT : k <= 1 };

          then

          consider kk be Element of NAT such that

           A2: x = (p |^ kk) & kk <= 1;

          kk = 0 or ... or kk = 1 by A2;

          then x = 1 or x = (p |^ 1) by NEWTON: 4, A2;

          hence thesis by TARSKI:def 2;

        end;

        let x be object;

        assume x in {1, p};

        then x = 1 or x = p by TARSKI:def 2;

        then x = (p |^ 0 ) or x = (p |^ 1) by NEWTON: 4;

        hence thesis;

      end;

      hence thesis by a1;

    end;

    theorem :: LATSTONE:27

    

     DivisorsSquare: for p be Prime holds ( NatDivisors (p * p)) = {1, p, (p * p)}

    proof

      let p be Prime;

      

       a1: ( NatDivisors (p |^ 2)) = { (p |^ k) where k be Element of NAT : k <= 2 } by NAT_5: 19;

      { (p |^ k) where k be Element of NAT : k <= 2 } = {1, p, (p * p)}

      proof

        thus { (p |^ k) where k be Element of NAT : k <= 2 } c= {1, p, (p * p)}

        proof

          let x be object;

          assume x in { (p |^ k) where k be Element of NAT : k <= 2 };

          then

          consider kk be Element of NAT such that

           A2: x = (p |^ kk) & kk <= 2;

          kk = 0 or ... or kk = 2 by A2;

          then x = 1 or x = p or x = (p * p) by A2, NEWTON: 81, NEWTON: 4;

          hence thesis by ENUMSET1:def 1;

        end;

        let x be object;

        assume x in {1, p, (p * p)};

        then x = 1 or x = p or x = (p * p) by ENUMSET1:def 1;

        then x = (p |^ 0 ) or x = (p |^ 1) or x = (p |^ 2) by NEWTON: 4, NEWTON: 81;

        hence thesis;

      end;

      hence thesis by a1, NEWTON: 81;

    end;

    registration

      let n be non zero Nat;

      cluster ( Divisors_Lattice n) -> finite;

      coherence

      proof

        ( NatDivisors n) is finite;

        hence thesis by MOEBIUS2:def 10;

      end;

    end

    registration

      cluster complete for Boolean Lattice;

      existence

      proof

        reconsider n = 1 as non zero Nat;

        set L = ( Divisors_Lattice n);

        L is Boolean by MOEBIUS1: 22;

        hence thesis;

      end;

    end

    registration

      let p be Prime;

      cluster ( Divisors_Lattice p) -> Boolean;

      coherence

      proof

        p is square-free by MOEBIUS1: 23;

        hence thesis;

      end;

    end

    registration

      let p be Prime;

      cluster ( Divisors_Lattice (p * p)) -> pseudocomplemented;

      coherence

      proof

        set L = ( Divisors_Lattice (p * p));

        the carrier of ( Divisors_Lattice (p * p)) = ( NatDivisors (p * p)) by MOEBIUS2:def 10;

        then

         A1: the carrier of L = {1, p, (p * p)} by DivisorsSquare;

        for x be Element of L holds ex y be Element of L st y is_a_pseudocomplement_of x

        proof

          let x be Element of L;

          per cases by ENUMSET1:def 1, A1;

            suppose

             C1: x = 1;

            reconsider pp = (p * p) as Element of L by A1, ENUMSET1:def 1;

            x = ( Bottom L) by C1, MOEBIUS2: 64;

            then

             B1: (pp "/\" x) = ( Bottom L);

            for y be Element of L st (x "/\" y) = ( Bottom L) holds y [= pp

            proof

              let y be Element of L;

              assume (x "/\" y) = ( Bottom L);

              pp = ( Top L) by MOEBIUS2: 64;

              hence thesis by LATTICES: 19;

            end;

            then pp is_a_pseudocomplement_of x by B1;

            hence thesis;

          end;

            suppose

             B0: x = p;

            reconsider pp = ( Bottom L) as Element of L;

            for y be Element of L st (x "/\" y) = ( Bottom L) holds y [= pp

            proof

              let y be Element of L;

              

               w3: y = 1 or y = p or y = (p * p) by A1, ENUMSET1:def 1;

              assume

               W1: (x "/\" y) = ( Bottom L);

              

               W2: y <> ( Top L)

              proof

                assume y = ( Top L);

                then p = 1 by B0, MOEBIUS2: 64, W1;

                hence thesis by INT_2:def 4;

              end;

              y <> p

              proof

                assume y = p;

                then 1 = p by W1, MOEBIUS2: 64, B0;

                hence thesis by INT_2:def 4;

              end;

              hence thesis by W2, w3, MOEBIUS2: 64;

            end;

            then pp is_a_pseudocomplement_of x;

            hence thesis;

          end;

            suppose

             C1: x = (p * p);

            reconsider pp = 1 as Element of L by A1, ENUMSET1:def 1;

            

             b1: pp = ( Bottom L) by MOEBIUS2: 64;

            for y be Element of L st (x "/\" y) = ( Bottom L) holds y [= pp

            proof

              let y be Element of L;

              assume

               S1: (x "/\" y) = ( Bottom L);

              

               s3: y = 1 or y = (p * p) or y = p by A1, ENUMSET1:def 1;

              

               R2: ( Top L) = (p * p) by MOEBIUS2: 64;

              y <> p

              proof

                assume y = p;

                then p = 1 by MOEBIUS2: 64, S1, R2, C1;

                hence thesis by INT_2:def 4;

              end;

              hence thesis by s3, C1, MOEBIUS2: 64, S1;

            end;

            then pp is_a_pseudocomplement_of x by b1;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

    end

    theorem :: LATSTONE:28

    

     PsCompl: for L be Lattice, p be Prime, x be Element of L st L = ( Divisors_Lattice (p * p)) & x = p holds (x * ) = ( Bottom L)

    proof

      let L be Lattice, p be Prime, x be Element of L;

      assume that

       A1: L = ( Divisors_Lattice (p * p)) and

       B0: x = p;

      reconsider pp = ( Bottom L) as Element of L;

      for y be Element of L st (x "/\" y) = ( Bottom L) holds y [= pp

      proof

        let y be Element of L;

        y in the carrier of L;

        then y in ( NatDivisors (p * p)) by A1, MOEBIUS2:def 10;

        then y in {1, p, (p * p)} by DivisorsSquare;

        then

         w3: y = 1 or y = p or y = (p * p) by ENUMSET1:def 1;

        assume

         W1: (x "/\" y) = ( Bottom L);

        

         W2: y <> ( Top L)

        proof

          assume y = ( Top L);

          then x = 1 by MOEBIUS2: 64, A1, W1;

          hence thesis by INT_2:def 4, B0;

        end;

        y <> p

        proof

          assume y = p;

          then 1 = p by A1, MOEBIUS2: 64, B0, W1;

          hence thesis by INT_2:def 4;

        end;

        hence thesis by W2, w3, A1, MOEBIUS2: 64;

      end;

      then pp is_a_pseudocomplement_of x by A1;

      hence thesis by def3, A1;

    end;

    registration

      let p be Prime;

      cluster ( Divisors_Lattice (p * p)) -> satisfying_Stone_identity;

      coherence

      proof

        set L = ( Divisors_Lattice (p * p));

        let x be Element of L;

        x in the carrier of L;

        then x in ( NatDivisors (p * p)) by MOEBIUS2:def 10;

        then x in {1, p, (p * p)} by DivisorsSquare;

        per cases by ENUMSET1:def 1;

          suppose x = 1;

          then x = ( Bottom L) by MOEBIUS2: 64;

          then (x * ) = ( Top L) by Th11;

          hence thesis;

        end;

          suppose x = p;

          then (x * ) = ( Bottom L) by PsCompl;

          hence thesis by Th11;

        end;

          suppose x = (p * p);

          then x = ( Top L) by MOEBIUS2: 64;

          then (x * ) = ( Bottom L) by Th11a;

          hence thesis by Th11;

        end;

      end;

    end

    registration

      let p be Prime;

      cluster ( Divisors_Lattice (p * p)) -> non Boolean Stone;

      coherence

      proof

        (p |^ 2) divides (p * p) by NEWTON: 81;

        then (p * p) is square-containing by MOEBIUS1:def 1;

        hence thesis by MOEBIUS2: 65;

      end;

    end

    registration

      cluster Stone non Boolean for Lattice;

      existence

      proof

        set p = the Prime;

        take ( Divisors_Lattice (p * p));

        thus thesis;

      end;

    end

    begin

    reserve L1,L2 for Lattice;

    reserve p1,q1 for Element of L1;

    reserve p2,q2 for Element of L2;

    theorem :: LATSTONE:29

    

     ProductPsCompl: L1 is 01_Lattice & L2 is 01_Lattice implies (p1 is_a_pseudocomplement_of q1 & p2 is_a_pseudocomplement_of q2 iff [p1, p2] is_a_pseudocomplement_of [q1, q2])

    proof

      assume

       A0: L1 is 01_Lattice & L2 is 01_Lattice;

      set L = [:L1, L2:];

      thus p1 is_a_pseudocomplement_of q1 & p2 is_a_pseudocomplement_of q2 implies [p1, p2] is_a_pseudocomplement_of [q1, q2]

      proof

        assume

         A1: p1 is_a_pseudocomplement_of q1 & p2 is_a_pseudocomplement_of q2;

        set a = [p1, p2], b = [q1, q2];

        

         a2: (a "/\" b) = [( Bottom L1), ( Bottom L2)] by A1, FILTER_1: 35;

        for x be Element of L st (b "/\" x) = ( Bottom L) holds x [= a

        proof

          let x be Element of L;

          assume

           Z1: (b "/\" x) = ( Bottom L);

          consider x1,x2 be object such that

           Z2: x1 in the carrier of L1 & x2 in the carrier of L2 & x = [x1, x2] by ZFMISC_1:def 2;

          reconsider x1 as Element of L1 by Z2;

          reconsider x2 as Element of L2 by Z2;

          ( [q1, q2] "/\" [x1, x2]) = [( Bottom L1), ( Bottom L2)] by FILTER_1: 42, A0, Z2, Z1;

          then

           Z3: [(q1 "/\" x1), (q2 "/\" x2)] = [( Bottom L1), ( Bottom L2)] by FILTER_1: 35;

          then

           T1: (q1 "/\" x1) = ( Bottom L1) by XTUPLE_0: 1;

          

           T2: (q2 "/\" x2) = ( Bottom L2) by Z3, XTUPLE_0: 1;

          

           Z4: x1 [= p1 by T1, A1;

          x2 [= p2 by A1, T2;

          hence thesis by Z2, FILTER_1: 36, Z4;

        end;

        hence thesis by a2, FILTER_1: 42, A0;

      end;

      assume

       W0: [p1, p2] is_a_pseudocomplement_of [q1, q2];

      then ( [p1, p2] "/\" [q1, q2]) = [( Bottom L1), ( Bottom L2)] by A0, FILTER_1: 42;

      then

       w1: [(p1 "/\" q1), (p2 "/\" q2)] = [( Bottom L1), ( Bottom L2)] by FILTER_1: 35;

      then

       W1: (p1 "/\" q1) = ( Bottom L1) & (p2 "/\" q2) = ( Bottom L2) by XTUPLE_0: 1;

      

       w2: for xx1 be Element of L1 st (q1 "/\" xx1) = ( Bottom L1) holds xx1 [= p1

      proof

        let xx1 be Element of L1;

        assume (q1 "/\" xx1) = ( Bottom L1);

        then [(q1 "/\" xx1), (q2 "/\" p2)] = ( Bottom [:L1, L2:]) by W1, FILTER_1: 42, A0;

        then ( [q1, q2] "/\" [xx1, p2]) = ( Bottom [:L1, L2:]) by FILTER_1: 35;

        then [xx1, p2] [= [p1, p2] by W0;

        hence thesis by FILTER_1: 36;

      end;

      for xx2 be Element of L2 st (q2 "/\" xx2) = ( Bottom L2) holds xx2 [= p2

      proof

        let xx2 be Element of L2;

        assume (q2 "/\" xx2) = ( Bottom L2);

        then [(q1 "/\" p1), (q2 "/\" xx2)] = ( Bottom [:L1, L2:]) by W1, FILTER_1: 42, A0;

        then ( [q1, q2] "/\" [p1, xx2]) = ( Bottom [:L1, L2:]) by FILTER_1: 35;

        then [p1, xx2] [= [p1, p2] by W0;

        hence thesis by FILTER_1: 36;

      end;

      hence thesis by w2, w1, XTUPLE_0: 1;

    end;

    theorem :: LATSTONE:30

    

     PsComplProduct: L1 is 01_Lattice & L2 is 01_Lattice implies (L1 is pseudocomplemented & L2 is pseudocomplemented iff [:L1, L2:] is pseudocomplemented)

    proof

      assume

       A0: L1 is 01_Lattice & L2 is 01_Lattice;

      thus L1 is pseudocomplemented & L2 is pseudocomplemented implies [:L1, L2:] is pseudocomplemented

      proof

        assume

         A1: L1 is pseudocomplemented & L2 is pseudocomplemented;

        for x be Element of [:L1, L2:] holds ex y be Element of [:L1, L2:] st y is_a_pseudocomplement_of x

        proof

          let x be Element of [:L1, L2:];

          consider x1,x2 be object such that

           B1: x1 in the carrier of L1 & x2 in the carrier of L2 & x = [x1, x2] by ZFMISC_1:def 2;

          reconsider x1 as Element of L1 by B1;

          reconsider x2 as Element of L2 by B1;

          consider xx1 be Element of L1 such that

           A2: xx1 is_a_pseudocomplement_of x1 by A1;

          consider xx2 be Element of L2 such that

           A3: xx2 is_a_pseudocomplement_of x2 by A1;

          take y = [xx1, xx2];

          thus thesis by B1, A2, A3, ProductPsCompl, A0;

        end;

        hence thesis;

      end;

      assume

       aa: [:L1, L2:] is pseudocomplemented;

      for x be Element of L1 holds ex y be Element of L1 st y is_a_pseudocomplement_of x

      proof

        let x be Element of L1;

        set x2 = the Element of L2;

        consider y be Element of [:L1, L2:] such that

         B0: y is_a_pseudocomplement_of [x, x2] by aa;

        consider y1,y2 be object such that

         B1: y1 in the carrier of L1 & y2 in the carrier of L2 & y = [y1, y2] by ZFMISC_1:def 2;

        reconsider y1 as Element of L1 by B1;

        reconsider y2 as Element of L2 by B1;

        take y1;

        thus thesis by B1, B0, ProductPsCompl, A0;

      end;

      hence L1 is pseudocomplemented;

      for x be Element of L2 holds ex y be Element of L2 st y is_a_pseudocomplement_of x

      proof

        let x be Element of L2;

        set x2 = the Element of L1;

        consider y be Element of [:L1, L2:] such that

         B0: y is_a_pseudocomplement_of [x2, x] by aa;

        consider y1,y2 be object such that

         B1: y1 in the carrier of L1 & y2 in the carrier of L2 & y = [y1, y2] by ZFMISC_1:def 2;

        reconsider y1 as Element of L1 by B1;

        reconsider y2 as Element of L2 by B1;

        take y2;

        thus thesis by B1, B0, ProductPsCompl, A0;

      end;

      hence thesis;

    end;

    registration

      let L1,L2 be pseudocomplemented 01_Lattice;

      cluster [:L1, L2:] -> pseudocomplemented;

      coherence by PsComplProduct;

    end

    theorem :: LATSTONE:31

    

     ProductPCompl: L1 is pseudocomplemented 01_Lattice & L2 is pseudocomplemented 01_Lattice implies ( [p1, p2] * ) = [(p1 * ), (p2 * )]

    proof

      assume

       A1: L1 is pseudocomplemented 01_Lattice & L2 is pseudocomplemented 01_Lattice;

      

       A3: (p1 * ) is_a_pseudocomplement_of p1 by def3, A1;

      (p2 * ) is_a_pseudocomplement_of p2 by def3, A1;

      then [(p1 * ), (p2 * )] is_a_pseudocomplement_of [p1, p2] by A3, ProductPsCompl, A1;

      hence thesis by def3, A1;

    end;

    reserve L1,L2 for non empty Lattice;

    theorem :: LATSTONE:32

    

     ProductIsSStone: L1 is satisfying_Stone_identity pseudocomplemented 01_Lattice & L2 is satisfying_Stone_identity pseudocomplemented 01_Lattice implies [:L1, L2:] is satisfying_Stone_identity

    proof

      assume that

       A1: L1 is satisfying_Stone_identity pseudocomplemented 01_Lattice and

       A2: L2 is satisfying_Stone_identity pseudocomplemented 01_Lattice;

      set L = [:L1, L2:];

      for x be Element of L holds ((x * ) "\/" ((x * ) * )) = ( Top L)

      proof

        let x be Element of L;

        consider x1,x2 be object such that

         A3: x1 in the carrier of L1 & x2 in the carrier of L2 & x = [x1, x2] by ZFMISC_1:def 2;

        reconsider x1 as Element of L1 by A3;

        reconsider x2 as Element of L2 by A3;

        

         X1: [(x1 * ), (x2 * )] = (x * ) by ProductPCompl, A3, A1, A2;

        

         A4: ((x1 * ) "\/" ((x1 * ) * )) = ( Top L1) by A1, SatStone;

         [((x1 * ) "\/" ((x1 * ) * )), ((x2 * ) "\/" ((x2 * ) * ))] = [( Top L1), ( Top L2)] by A4, A2, SatStone

        .= ( Top L) by FILTER_1: 43, A1, A2;

        

        then ( Top L) = ( [(x1 * ), (x2 * )] "\/" [((x1 * ) * ), ((x2 * ) * )]) by FILTER_1: 35

        .= ((x * ) "\/" ((x * ) * )) by X1, ProductPCompl, A1, A2;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: LATSTONE:33

    L1 is Stone & L2 is Stone implies [:L1, L2:] is Stone by ProductIsSStone, FILTER_1: 38;

    registration

      let L1,L2 be Stone Lattice;

      cluster [:L1, L2:] -> Stone;

      coherence by ProductIsSStone, FILTER_1: 38;

    end

    begin

    reserve B for Boolean Lattice;

    definition

      let B be Boolean Lattice;

      :: LATSTONE:def12

      func B squared -> Subset of [:B, B:] equals { [a, b] where a,b be Element of B : a [= b };

      coherence

      proof

        { [a, b] where a,b be Element of B : a [= b } c= the carrier of [:B, B:]

        proof

          let x be object;

          assume x in { [a, b] where a,b be Element of B : a [= b };

          then

          consider a1,b1 be Element of B such that

           A1: x = [a1, b1] & a1 [= b1;

          thus thesis by A1;

        end;

        hence thesis;

      end;

    end

    registration

      let B be Boolean Lattice;

      cluster (B squared ) -> non empty;

      coherence

      proof

        set x = ( Bottom B);

        take [x, x];

        thus thesis;

      end;

    end

    registration

      let B be Boolean Lattice;

      cluster (B squared ) -> join-closed meet-closed;

      coherence

      proof

        set S = (B squared );

        

         AA: for p,q be Element of [:B, B:] st p in S & q in S holds (p "\/" q) in S

        proof

          let p,q be Element of [:B, B:];

          assume

           A0: p in S & q in S;

          then

          consider a1,b1 be Element of B such that

           A1: p = [a1, b1] & a1 [= b1;

          consider a2,b2 be Element of B such that

           A2: q = [a2, b2] & a2 [= b2 by A0;

          

           A3: (p "\/" q) = [(a1 "\/" a2), (b1 "\/" b2)] by FILTER_1: 35, A1, A2;

          (a1 "\/" a2) [= (b1 "\/" b2) by A1, A2, FILTER_0: 4;

          hence thesis by A3;

        end;

        for p,q be Element of [:B, B:] st p in S & q in S holds (p "/\" q) in S

        proof

          let p,q be Element of [:B, B:];

          assume

           A0: p in S & q in S;

          then

          consider a1,b1 be Element of B such that

           A1: p = [a1, b1] & a1 [= b1;

          consider a2,b2 be Element of B such that

           A2: q = [a2, b2] & a2 [= b2 by A0;

          

           A3: (p "/\" q) = [(a1 "/\" a2), (b1 "/\" b2)] by FILTER_1: 35, A1, A2;

          (a1 "/\" a2) [= (b1 "/\" b2) by A1, A2, FILTER_0: 5;

          hence thesis by A3;

        end;

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

      end;

    end

    definition

      let B be Boolean Lattice;

      :: original: squared

      redefine

      func B squared -> non empty ClosedSubset of [:B, B:] ;

      coherence ;

    end

    definition

      let B be Boolean Lattice;

      :: LATSTONE:def13

      func B squared-latt -> Lattice equals ( latt ( [:B, B:],(B squared )));

      coherence ;

    end

    theorem :: LATSTONE:34

    

     SquaredCarrier: the carrier of (B squared-latt ) = (B squared )

    proof

      set L = [:B, B:];

      set P = (B squared );

      consider o1,o2 be BinOp of P such that

       A1: o1 = (the L_join of L || P) & o2 = (the L_meet of L || P) & ( latt ( [:B, B:],P)) = LattStr (# P, o1, o2 #) by FILTER_2:def 14;

      thus thesis by A1;

    end;

    theorem :: LATSTONE:35

     [( Bottom B), ( Bottom B)] in the carrier of (B squared-latt )

    proof

       [( Bottom B), ( Bottom B)] in (B squared );

      hence thesis by SquaredCarrier;

    end;

    theorem :: LATSTONE:36

     [( Top B), ( Top B)] in the carrier of (B squared-latt )

    proof

       [( Top B), ( Top B)] in (B squared );

      hence thesis by SquaredCarrier;

    end;

    registration

      let B be Boolean Lattice;

      cluster (B squared-latt ) -> lower-bounded;

      coherence

      proof

        ( Bottom [:B, B:]) = [( Bottom B), ( Bottom B)] by FILTER_1: 42;

        then ( Bottom [:B, B:]) in (B squared );

        hence thesis by ThB;

      end;

      cluster (B squared-latt ) -> upper-bounded;

      coherence

      proof

        ( Top [:B, B:]) = [( Top B), ( Top B)] by FILTER_1: 43;

        then ( Top [:B, B:]) in (B squared );

        hence thesis by ThC;

      end;

    end

    theorem :: LATSTONE:37

    

     SquaredBottom: ( Bottom (B squared-latt )) = [( Bottom B), ( Bottom B)]

    proof

       [( Bottom B), ( Bottom B)] in (B squared );

      then ( Bottom [:B, B:]) in (B squared ) by FILTER_1: 42;

      then ( Bottom ( latt ( [:B, B:],(B squared )))) = ( Bottom [:B, B:]) by ThB;

      hence thesis by FILTER_1: 42;

    end;

    theorem :: LATSTONE:38

    

     SquaredTop: ( Top (B squared-latt )) = [( Top B), ( Top B)]

    proof

       [( Top B), ( Top B)] in (B squared );

      then ( Top [:B, B:]) in (B squared ) by FILTER_1: 43;

      then ( Top ( latt ( [:B, B:],(B squared )))) = ( Top [:B, B:]) by ThC;

      hence thesis by FILTER_1: 43;

    end;

    registration

      let B be Boolean Lattice;

      cluster (B squared-latt ) -> pseudocomplemented;

      coherence

      proof

        set L = (B squared-latt );

        for x be Element of L holds ex y be Element of L st y is_a_pseudocomplement_of x

        proof

          let x be Element of L;

          x in the carrier of L;

          then x in (B squared ) by SquaredCarrier;

          then

          consider x1,x2 be Element of B such that

           A1: x = [x1, x2] & x1 [= x2;

          

           I1: [(x2 ` ), (x2 ` )] in (B squared );

          reconsider y = [(x2 ` ), (x2 ` )] as Element of L by I1, SquaredCarrier;

          take y;

          

           Z1: (x "/\" y) = ( [x1, x2] "/\" [(x2 ` ), (x2 ` )]) by A1, MSUALG_7: 11

          .= [(x1 "/\" (x2 ` )), (x2 "/\" (x2 ` ))] by FILTER_1: 35

          .= [(x1 "/\" (x2 ` )), ( Bottom B)] by LATTICES: 20;

          (x2 ` ) [= (x1 ` ) by A1, LATTICES: 26;

          then (x1 "/\" (x2 ` )) [= (x1 "/\" (x1 ` )) by FILTER_0: 5;

          then (x1 "/\" (x2 ` )) [= ( Bottom B) by LATTICES: 20;

          then

           tt: (x1 "/\" (x2 ` )) = ( Bottom B) by BOOLEALG: 9;

          for w be Element of L st (x "/\" w) = ( Bottom L) holds w [= y

          proof

            let w be Element of L;

            assume

             O1: (x "/\" w) = ( Bottom L);

            w in the carrier of L;

            then w in (B squared ) by SquaredCarrier;

            then

            consider w1,w2 be Element of B such that

             Y1: w = [w1, w2] & w1 [= w2;

            ( [x1, x2] "/\" [w1, w2]) = ( Bottom L) by O1, Y1, A1, MSUALG_7: 11;

            then ( [x1, x2] "/\" [w1, w2]) = [( Bottom B), ( Bottom B)] by SquaredBottom;

            then [(x1 "/\" w1), (x2 "/\" w2)] = [( Bottom B), ( Bottom B)] by FILTER_1: 35;

            then (x1 "/\" w1) = ( Bottom B) & (x2 "/\" w2) = ( Bottom B) by XTUPLE_0: 1;

            then

             Y2: w2 [= (x2 ` ) by LATTICES: 25;

            then w1 [= (x2 ` ) by Y1, LATTICES: 7;

            then ( [w1, w2] "/\" [(x2 ` ), (x2 ` )]) = [w1, w2] by LATTICES: 4, Y2, FILTER_1: 36;

            then (w "/\" y) = w by Y1, MSUALG_7: 11;

            hence thesis by LATTICES: 4;

          end;

          hence thesis by tt, Z1, SquaredBottom;

        end;

        hence thesis;

      end;

    end

    theorem :: LATSTONE:39

    

     PseudoInSquared: for L be Lattice, x1,x2 be Element of B, x be Element of L st L = (B squared-latt ) & x = [x1, x2] holds (x * ) = [(x2 ` ), (x2 ` )]

    proof

      let L be Lattice, x1,x2 be Element of B, x be Element of L;

      assume

       A0: L = (B squared-latt ) & x = [x1, x2];

      x in the carrier of L;

      then x in (B squared ) by SquaredCarrier, A0;

      then

      consider xx1,xx2 be Element of B such that

       W1: x = [xx1, xx2] & xx1 [= xx2;

      

       aa: xx1 = x1 & xx2 = x2 by W1, A0, XTUPLE_0: 1;

       [(x2 ` ), (x2 ` )] in (B squared );

      then

      reconsider y = [(x2 ` ), (x2 ` )] as Element of L by A0, SquaredCarrier;

      

       Z1: (x "/\" y) = ( [x1, x2] "/\" [(x2 ` ), (x2 ` )]) by A0, MSUALG_7: 11

      .= [(x1 "/\" (x2 ` )), (x2 "/\" (x2 ` ))] by FILTER_1: 35

      .= [(x1 "/\" (x2 ` )), ( Bottom B)] by LATTICES: 20;

      (x2 ` ) [= (x1 ` ) by aa, W1, LATTICES: 26;

      then (x1 "/\" (x2 ` )) [= (x1 "/\" (x1 ` )) by FILTER_0: 5;

      then (x1 "/\" (x2 ` )) [= ( Bottom B) by LATTICES: 20;

      then

       tt: (x1 "/\" (x2 ` )) = ( Bottom B) by BOOLEALG: 9;

      for w be Element of L st (x "/\" w) = ( Bottom L) holds w [= y

      proof

        let w be Element of L;

        assume

         O1: (x "/\" w) = ( Bottom L);

        w in the carrier of L;

        then w in (B squared ) by A0, SquaredCarrier;

        then

        consider w1,w2 be Element of B such that

         Y1: w = [w1, w2] & w1 [= w2;

        ( [x1, x2] "/\" [w1, w2]) = ( Bottom L) by O1, Y1, A0, MSUALG_7: 11;

        then ( [x1, x2] "/\" [w1, w2]) = [( Bottom B), ( Bottom B)] by A0, SquaredBottom;

        then [(x1 "/\" w1), (x2 "/\" w2)] = [( Bottom B), ( Bottom B)] by FILTER_1: 35;

        then (x1 "/\" w1) = ( Bottom B) & (x2 "/\" w2) = ( Bottom B) by XTUPLE_0: 1;

        then

         Y2: w2 [= (x2 ` ) by LATTICES: 25;

        then w1 [= (x2 ` ) by Y1, LATTICES: 7;

        then ( [w1, w2] "/\" [(x2 ` ), (x2 ` )]) = [w1, w2] by LATTICES: 4, Y2, FILTER_1: 36;

        then (w "/\" y) = w by Y1, MSUALG_7: 11, A0;

        hence thesis by LATTICES: 4;

      end;

      then y is_a_pseudocomplement_of x by tt, Z1, A0, SquaredBottom;

      hence thesis by def3, A0;

    end;

    registration

      let B be Boolean Lattice;

      cluster (B squared-latt ) -> satisfying_Stone_identity;

      coherence

      proof

        set L = (B squared-latt );

        for x be Element of L holds ((x * ) "\/" ((x * ) * )) = ( Top L)

        proof

          let x be Element of L;

          x in the carrier of L;

          then x in (B squared ) by SquaredCarrier;

          then

          consider x1,x2 be Element of B such that

           W1: x = [x1, x2] & x1 [= x2;

           [(x2 ` ), (x2 ` )] in (B squared );

          then

          reconsider y = [(x2 ` ), (x2 ` )] as Element of L by SquaredCarrier;

          

           W0: (x * ) = [(x2 ` ), (x2 ` )] by W1, PseudoInSquared;

          then ((x * ) * ) = [((x2 ` ) ` ), ((x2 ` ) ` )] by PseudoInSquared;

          

          then ((x * ) "\/" ((x * ) * )) = ( [(x2 ` ), (x2 ` )] "\/" [x2, x2]) by W0, MSUALG_7: 11

          .= [((x2 ` ) "\/" x2), ((x2 ` ) "\/" x2)] by FILTER_1: 35

          .= [( Top B), ((x2 ` ) "\/" x2)] by LATTICES: 21

          .= [( Top B), ( Top B)] by LATTICES: 21

          .= ( Top L) by SquaredTop;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let B be Boolean Lattice;

      cluster (B squared-latt ) -> Stone;

      coherence ;

    end

    theorem :: LATSTONE:40

    ( Skeleton (B squared-latt )) = the set of all [a, a] where a be Element of B

    proof

      set L = (B squared-latt );

      ( Skeleton (B squared-latt )) = the set of all [a, a] where a be Element of B

      proof

        thus ( Skeleton (B squared-latt )) c= the set of all [a, a] where a be Element of B

        proof

          let x be object;

          assume x in ( Skeleton L);

          then

          consider a be Element of L such that

           A1: x = (a * );

          a in the carrier of L;

          then a in (B squared ) by SquaredCarrier;

          then

          consider a1,a2 be Element of B such that

           A2: a = [a1, a2] & a1 [= a2;

          (a * ) = [(a2 ` ), (a2 ` )] by A2, PseudoInSquared;

          hence thesis by A1;

        end;

        let x be object;

        assume x in the set of all [a, a] where a be Element of B;

        then

        consider a be Element of B such that

         B1: x = [a, a];

        set b = [(a ` ), (a ` )];

        b in (B squared );

        then

        reconsider b as Element of L by FILTER_2: 72;

        reconsider a1 = (b * ) as Element of L;

        (b * ) = [((a ` ) ` ), ((a ` ) ` )] by PseudoInSquared

        .= [a, a];

        hence thesis by B1;

      end;

      hence thesis;

    end;

    theorem :: LATSTONE:41

    ( DenseElements (B squared-latt )) = the set of all [a, ( Top B)] where a be Element of B

    proof

      set L = (B squared-latt );

      thus ( DenseElements L) c= the set of all [a, ( Top B)] where a be Element of B

      proof

        let x be object;

        assume x in ( DenseElements L);

        then

        consider a be Element of L such that

         A1: x = a & (a * ) = ( Bottom L);

        x in the carrier of L by A1;

        then x in (B squared ) by SquaredCarrier;

        then

        consider a1,a2 be Element of B such that

         A2: x = [a1, a2] & a1 [= a2;

        

         A3: (a * ) = [( Bottom B), ( Bottom B)] by A1, SquaredBottom;

        (a * ) = [(a2 ` ), (a2 ` )] by A1, A2, PseudoInSquared;

        then ((a2 ` ) ` ) = (( Bottom B) ` ) by A3, XTUPLE_0: 1;

        then a2 = ( Top B) by LATTICE4: 30;

        hence thesis by A2;

      end;

      let x be object;

      assume x in the set of all [a, ( Top B)] where a be Element of B;

      then

      consider a be Element of B such that

       A1: x = [a, ( Top B)];

      a [= ( Top B) by LATTICES: 19;

      then x in (B squared ) by A1;

      then

      reconsider y = x as Element of L by SquaredCarrier;

      (y * ) = [(( Top B) ` ), (( Top B) ` )] by A1, PseudoInSquared;

      

      then (y * ) = [( Bottom B), (( Top B) ` )] by LATTICE4: 29

      .= [( Bottom B), ( Bottom B)] by LATTICE4: 29

      .= ( Bottom L) by SquaredBottom;

      hence thesis;

    end;