sheffer1.miz



    begin

    theorem :: SHEFFER1:1

    

     Th1: for L be join-commutative join-associative Huntington non empty ComplLLattStr, a,b be Element of L holds ((a + b) ` ) = ((a ` ) *' (b ` ))

    proof

      let L be join-commutative join-associative Huntington non empty ComplLLattStr;

      let a,b be Element of L;

      (a + b) = (((a ` ) *' (b ` )) ` ) by ROBBINS1: 17;

      hence thesis by ROBBINS1: 3;

    end;

    begin

    definition

      let IT be non empty LattStr;

      :: SHEFFER1:def1

      attr IT is upper-bounded' means ex c be Element of IT st for a be Element of IT holds (c "/\" a) = a & (a "/\" c) = a;

    end

    definition

      let L be non empty LattStr;

      assume

       A1: L is upper-bounded';

      :: SHEFFER1:def2

      func Top' L -> Element of L means

      : Def2: for a be Element of L holds (it "/\" a) = a & (a "/\" it ) = a;

      existence by A1;

      uniqueness

      proof

        let c1,c2 be Element of L such that

         A2: for a be Element of L holds (c1 "/\" a) = a & (a "/\" c1) = a and

         A3: for a be Element of L holds (c2 "/\" a) = a & (a "/\" c2) = a;

        

        thus c1 = (c2 "/\" c1) by A3

        .= c2 by A2;

      end;

    end

    definition

      let IT be non empty LattStr;

      :: SHEFFER1:def3

      attr IT is lower-bounded' means ex c be Element of IT st for a be Element of IT holds (c "\/" a) = a & (a "\/" c) = a;

    end

    definition

      let L be non empty LattStr;

      assume

       A1: L is lower-bounded';

      :: SHEFFER1:def4

      func Bot' L -> Element of L means

      : Def4: for a be Element of L holds (it "\/" a) = a & (a "\/" it ) = a;

      existence by A1;

      uniqueness

      proof

        let c1,c2 be Element of L such that

         A2: for a be Element of L holds (c1 "\/" a) = a & (a "\/" c1) = a and

         A3: for a be Element of L holds (c2 "\/" a) = a & (a "\/" c2) = a;

        

        thus c1 = (c2 "\/" c1) by A3

        .= c2 by A2;

      end;

    end

    definition

      let IT be non empty LattStr;

      :: SHEFFER1:def5

      attr IT is distributive' means

      : Def5: for a,b,c be Element of IT holds (a "\/" (b "/\" c)) = ((a "\/" b) "/\" (a "\/" c));

    end

    definition

      let L be non empty LattStr, a,b be Element of L;

      :: SHEFFER1:def6

      pred a is_a_complement'_of b means (b "\/" a) = ( Top' L) & (a "\/" b) = ( Top' L) & (b "/\" a) = ( Bot' L) & (a "/\" b) = ( Bot' L);

    end

    definition

      let IT be non empty LattStr;

      :: SHEFFER1:def7

      attr IT is complemented' means

      : Def7: for b be Element of IT holds ex a be Element of IT st a is_a_complement'_of b;

    end

    definition

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

      assume

       A1: L is complemented' distributive upper-bounded' meet-commutative;

      :: SHEFFER1:def8

      func x `# -> Element of L means

      : Def8: it is_a_complement'_of x;

      existence by A1;

      uniqueness

      proof

        let a,b be Element of L such that

         A2: a is_a_complement'_of x and

         A3: b is_a_complement'_of x;

        b = (b "/\" ( Top' L)) by A1, Def2

        .= (b "/\" (x "\/" a)) by A2

        .= ((b "/\" x) "\/" (b "/\" a)) by A1

        .= ((x "/\" b) "\/" (b "/\" a)) by A1

        .= ((x "/\" b) "\/" (a "/\" b)) by A1

        .= (( Bot' L) "\/" (a "/\" b)) by A3

        .= ((a "/\" x) "\/" (a "/\" b)) by A2

        .= (a "/\" (x "\/" b)) by A1

        .= (a "/\" ( Top' L)) by A3

        .= a by A1, Def2;

        hence thesis;

      end;

    end

    registration

      cluster Boolean join-idempotent upper-bounded' complemented' distributive' lower-bounded' Lattice-like for 1 -element LattStr;

      existence

      proof

        set L = the 1 -element Lattice;

        

         A1: L is lower-bounded

        proof

          set x = the Element of L;

          for y be Element of L holds (x "/\" y) = x & (y "/\" x) = x by STRUCT_0:def 10;

          hence thesis;

        end;

        

         A2: L is upper-bounded

        proof

          set x = the Element of L;

          for y be Element of L holds (x "\/" y) = x & (y "\/" x) = x by STRUCT_0:def 10;

          hence thesis;

        end;

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

        proof

          let b be Element of L;

          take a = b;

          (b "\/" a) = ( Top L) & (b "/\" a) = ( Bottom L) by STRUCT_0:def 10;

          hence thesis;

        end;

        then

         A3: L is complemented;

        

         A4: L is join-idempotent;

        for b be Element of L holds ex a be Element of L st a is_a_complement'_of b

        proof

          let b be Element of L;

          take a = b;

          (b "\/" a) = ( Top' L) & (b "/\" a) = ( Bot' L) by STRUCT_0:def 10;

          hence thesis;

        end;

        then

         A5: L is complemented';

        for a,b,c be Element of L holds (a "/\" (b "\/" c)) = ((a "/\" b) "\/" (a "/\" c)) by STRUCT_0:def 10;

        then

         A6: L is distributive;

        

         A7: L is lower-bounded'

        proof

          set x = the Element of L;

          for y be Element of L holds (x "\/" y) = y & (y "\/" x) = y by STRUCT_0:def 10;

          hence thesis;

        end;

        

         A8: L is upper-bounded'

        proof

          set x = the Element of L;

          for y be Element of L holds (x "/\" y) = y & (y "/\" x) = y by STRUCT_0:def 10;

          hence thesis;

        end;

        for a,b,c be Element of L holds (a "\/" (b "/\" c)) = ((a "\/" b) "/\" (a "\/" c)) by STRUCT_0:def 10;

        then L is distributive';

        hence thesis by A3, A6, A1, A2, A4, A8, A5, A7;

      end;

    end

    theorem :: SHEFFER1:2

    

     Th2: for L be complemented' join-commutative meet-commutative distributive upper-bounded' distributive' non empty LattStr holds for x be Element of L holds (x "\/" (x `# )) = ( Top' L)

    proof

      let L be complemented' join-commutative meet-commutative distributive upper-bounded' distributive' non empty LattStr;

      let x be Element of L;

      (x `# ) is_a_complement'_of x by Def8;

      hence thesis;

    end;

    theorem :: SHEFFER1:3

    

     Th3: for L be complemented' join-commutative meet-commutative distributive upper-bounded' distributive' non empty LattStr holds for x be Element of L holds (x "/\" (x `# )) = ( Bot' L)

    proof

      let L be complemented' join-commutative meet-commutative distributive upper-bounded' distributive' non empty LattStr;

      let x be Element of L;

      (x `# ) is_a_complement'_of x by Def8;

      hence thesis;

    end;

    theorem :: SHEFFER1:4

    

     Th4: for L be complemented' join-commutative meet-commutative join-idempotent distributive upper-bounded' distributive' non empty LattStr holds for x be Element of L holds (x "\/" ( Top' L)) = ( Top' L)

    proof

      let L be complemented' join-commutative meet-commutative join-idempotent distributive upper-bounded' distributive' non empty LattStr;

      let x be Element of L;

      (x "\/" ( Top' L)) = ((x "\/" ( Top' L)) "/\" ( Top' L)) by Def2

      .= ((x "\/" ( Top' L)) "/\" (x "\/" (x `# ))) by Th2

      .= (x "\/" (( Top' L) "/\" (x `# ))) by Def5

      .= (x "\/" (x `# )) by Def2

      .= ( Top' L) by Th2;

      hence thesis;

    end;

    theorem :: SHEFFER1:5

    

     Th5: for L be complemented' join-commutative meet-commutative join-idempotent distributive upper-bounded' lower-bounded' distributive' non empty LattStr holds for x be Element of L holds (x "/\" ( Bot' L)) = ( Bot' L)

    proof

      let L be complemented' join-commutative meet-commutative join-idempotent distributive upper-bounded' lower-bounded' distributive' non empty LattStr;

      let x be Element of L;

      (x "/\" ( Bot' L)) = ((x "/\" ( Bot' L)) "\/" ( Bot' L)) by Def4

      .= ((x "/\" ( Bot' L)) "\/" (x "/\" (x `# ))) by Th3

      .= (x "/\" (( Bot' L) "\/" (x `# ))) by LATTICES:def 11

      .= (x "/\" (x `# )) by Def4

      .= ( Bot' L) by Th3;

      hence thesis;

    end;

    theorem :: SHEFFER1:6

    

     Th6: for L be join-commutative meet-absorbing meet-commutative join-absorbing join-idempotent distributive non empty LattStr holds for x,y,z be Element of L holds (((x "\/" y) "\/" z) "/\" x) = x

    proof

      let L be join-commutative meet-absorbing meet-commutative join-absorbing join-idempotent distributive non empty LattStr;

      let x,y,z be Element of L;

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

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

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

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

      .= x by LATTICES:def 8;

      hence thesis;

    end;

    theorem :: SHEFFER1:7

    

     Th7: for L be join-commutative meet-absorbing meet-commutative join-absorbing join-idempotent distributive' non empty LattStr holds for x,y,z be Element of L holds (((x "/\" y) "/\" z) "\/" x) = x

    proof

      let L be join-commutative meet-absorbing meet-commutative join-absorbing join-idempotent distributive' non empty LattStr;

      let x,y,z be Element of L;

      (((x "/\" y) "/\" z) "\/" x) = ((x "\/" (x "/\" y)) "/\" (x "\/" z)) by Def5

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

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

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

      .= x by LATTICES:def 9;

      hence thesis;

    end;

    definition

      let G be non empty /\-SemiLattStr;

      :: SHEFFER1:def9

      attr G is meet-idempotent means for x be Element of G holds (x "/\" x) = x;

    end

    theorem :: SHEFFER1:8

    

     Th8: for L be complemented' join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' non empty LattStr holds L is meet-idempotent

    proof

      let L be complemented' join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' non empty LattStr;

      now

        let x be Element of L;

        

        thus (x "/\" x) = ((x "/\" x) "\/" ( Bot' L)) by Def4

        .= ((x "/\" x) "\/" (x "/\" (x `# ))) by Th3

        .= (x "/\" (x "\/" (x `# ))) by LATTICES:def 11

        .= (x "/\" ( Top' L)) by Th2

        .= x by Def2;

      end;

      hence thesis;

    end;

    theorem :: SHEFFER1:9

    

     Th9: for L be complemented' join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' non empty LattStr holds L is join-idempotent

    proof

      let L be complemented' join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' non empty LattStr;

      let x be Element of L;

      

      thus (x "\/" x) = ((x "\/" x) "/\" ( Top' L)) by Def2

      .= ((x "\/" x) "/\" (x "\/" (x `# ))) by Th2

      .= (x "\/" (x "/\" (x `# ))) by Def5

      .= (x "\/" ( Bot' L)) by Th3

      .= x by Def4;

    end;

    theorem :: SHEFFER1:10

    

     Th10: for L be complemented' join-commutative meet-commutative join-idempotent distributive upper-bounded' distributive' non empty LattStr holds L is meet-absorbing

    proof

      let L be complemented' join-commutative meet-commutative join-idempotent distributive upper-bounded' distributive' non empty LattStr;

      let y,x be Element of L;

      (x "\/" (x "/\" y)) = ((( Top' L) "/\" x) "\/" (x "/\" y)) by Def2

      .= (x "/\" (( Top' L) "\/" y)) by LATTICES:def 11

      .= (x "/\" ( Top' L)) by Th4

      .= x by Def2;

      hence thesis;

    end;

    theorem :: SHEFFER1:11

    

     Th11: for L be complemented' join-commutative upper-bounded' meet-commutative join-idempotent distributive distributive' lower-bounded' non empty LattStr holds L is join-absorbing

    proof

      let L be complemented' join-commutative upper-bounded' meet-commutative join-idempotent distributive distributive' lower-bounded' non empty LattStr;

      let x,y be Element of L;

      

       A1: L is meet-idempotent by Th8;

      

       A2: L is meet-absorbing by Th10;

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

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

      .= x by A2;

      hence thesis;

    end;

    theorem :: SHEFFER1:12

    

     Th12: for L be complemented' join-commutative meet-commutative upper-bounded' lower-bounded' join-idempotent distributive distributive' non empty LattStr holds L is upper-bounded

    proof

      let L be complemented' join-commutative meet-commutative upper-bounded' lower-bounded' join-idempotent distributive distributive' non empty LattStr;

      ex c be Element of L st for a be Element of L holds (c "\/" a) = c & (a "\/" c) = c

      proof

        take ( Top' L);

        let a be Element of L;

        thus thesis by Th4;

      end;

      hence thesis;

    end;

    theorem :: SHEFFER1:13

    

     Th13: for L be Boolean Lattice-like non empty LattStr holds L is upper-bounded'

    proof

      let L be Boolean Lattice-like non empty LattStr;

      ex c be Element of L st for a be Element of L holds (c "/\" a) = a & (a "/\" c) = a

      proof

        take c = ( Top L);

        let a be Element of L;

        thus thesis;

      end;

      hence thesis;

    end;

    theorem :: SHEFFER1:14

    

     Th14: for L be complemented' join-commutative meet-commutative upper-bounded' lower-bounded' join-idempotent distributive distributive' non empty LattStr holds L is lower-bounded

    proof

      let L be complemented' join-commutative meet-commutative upper-bounded' lower-bounded' join-idempotent distributive distributive' non empty LattStr;

      ex c be Element of L st for a be Element of L holds (c "/\" a) = c & (a "/\" c) = c

      proof

        take ( Bot' L);

        let a be Element of L;

        thus thesis by Th5;

      end;

      hence thesis;

    end;

    theorem :: SHEFFER1:15

    

     Th15: for L be Boolean Lattice-like non empty LattStr holds L is lower-bounded'

    proof

      let L be Boolean Lattice-like non empty LattStr;

      ex c be Element of L st for a be Element of L holds (c "\/" a) = a & (a "\/" c) = a

      proof

        take c = ( Bottom L);

        let a be Element of L;

        thus thesis;

      end;

      hence thesis;

    end;

    theorem :: SHEFFER1:16

    

     Th16: for L be join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent distributive non empty LattStr holds L is join-associative

    proof

      let L be join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent distributive non empty LattStr;

      let x,y,z be Element of L;

      

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

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

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

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

      .= y by LATTICES:def 8;

      

       A2: (((x "\/" y) "\/" z) "/\" x) = x by Th6;

      (x "\/" (y "\/" z)) = ((x "\/" y) "\/" z)

      proof

        set A = (((x "\/" y) "\/" z) "/\" (x "\/" (y "\/" z)));

        

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

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

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

        .= ((x "\/" y) "\/" z) by A1, LATTICES:def 9;

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

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

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

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

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

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

        hence thesis by A3;

      end;

      hence thesis;

    end;

    theorem :: SHEFFER1:17

    

     Th17: for L be join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent distributive' non empty LattStr holds L is meet-associative

    proof

      let L be join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent distributive' non empty LattStr;

      let x,y,z be Element of L;

      

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

      

       A2: (((y "/\" z) "/\" x) "\/" y) = ((y "\/" (y "/\" z)) "/\" (y "\/" x)) by Def5

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

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

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

      .= y by LATTICES:def 9;

      (x "/\" (y "/\" z)) = ((x "/\" y) "/\" z)

      proof

        set A = (((x "/\" y) "/\" z) "\/" (x "/\" (y "/\" z)));

        

         A3: A = (((x "/\" y) "\/" (x "/\" (y "/\" z))) "/\" (z "\/" (x "/\" (y "/\" z)))) by Def5

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

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

        .= ((x "/\" y) "/\" z) by A2, LATTICES:def 8;

        A = ((((x "/\" y) "/\" z) "\/" x) "/\" (((x "/\" y) "/\" z) "\/" (y "/\" z))) by Def5

        .= (x "/\" ((((x "/\" y) "/\" z) "\/" y) "/\" (((x "/\" y) "/\" z) "\/" z))) by A1, Def5

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

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

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

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

        hence thesis by A3;

      end;

      hence thesis;

    end;

    theorem :: SHEFFER1:18

    

     Th18: for L be complemented' join-commutative meet-commutative lower-bounded' upper-bounded' join-idempotent distributive distributive' non empty LattStr holds ( Top L) = ( Top' L)

    proof

      let L be complemented' join-commutative meet-commutative lower-bounded' upper-bounded' join-idempotent distributive distributive' non empty LattStr;

      set Y = ( Top' L);

      L is upper-bounded & for a be Element of L holds (Y "\/" a) = Y & (a "\/" Y) = Y by Th4, Th12;

      hence thesis by LATTICES:def 17;

    end;

    theorem :: SHEFFER1:19

    

     Th19: for L be complemented' join-commutative meet-commutative lower-bounded' upper-bounded' join-idempotent distributive distributive' non empty LattStr holds ( Bottom L) = ( Bot' L)

    proof

      let L be complemented' join-commutative meet-commutative lower-bounded' upper-bounded' join-idempotent distributive distributive' non empty LattStr;

      set Y = ( Bot' L);

      L is lower-bounded & for a be Element of L holds (Y "/\" a) = Y & (a "/\" Y) = Y by Th5, Th14;

      hence thesis by LATTICES:def 16;

    end;

    theorem :: SHEFFER1:20

    

     Th20: for L be Boolean distributive' Lattice-like non empty LattStr holds ( Top L) = ( Top' L)

    proof

      let L be Boolean distributive' Lattice-like non empty LattStr;

      set Y = ( Top L);

      L is upper-bounded' & for a be Element of L holds (Y "/\" a) = a & (a "/\" Y) = a by Th13;

      hence thesis by Def2;

    end;

    theorem :: SHEFFER1:21

    

     Th21: for L be Boolean complemented lower-bounded upper-bounded distributive distributive' Lattice-like non empty LattStr holds ( Bottom L) = ( Bot' L)

    proof

      let L be Boolean complemented lower-bounded upper-bounded distributive distributive' Lattice-like non empty LattStr;

      set Y = ( Bottom L);

      L is lower-bounded' & for a be Element of L holds (Y "\/" a) = a & (a "\/" Y) = a by Th15;

      hence thesis by Def4;

    end;

    theorem :: SHEFFER1:22

    for L be complemented' lower-bounded' upper-bounded' join-commutative meet-commutative join-idempotent distributive distributive' non empty LattStr, x,y be Element of L holds x is_a_complement'_of y iff x is_a_complement_of y by Th19, Th18;

    theorem :: SHEFFER1:23

    

     Th23: for L be complemented' join-commutative meet-commutative lower-bounded' upper-bounded' join-idempotent distributive distributive' non empty LattStr holds L is complemented

    proof

      let L be complemented' join-commutative meet-commutative lower-bounded' upper-bounded' join-idempotent distributive distributive' non empty LattStr;

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

      proof

        let b be Element of L;

        consider a be Element of L such that

         A1: a is_a_complement'_of b by Def7;

        take a;

        

         A2: (b "/\" a) = ( Bot' L) by A1;

        (b "\/" a) = ( Top' L) by A1;

        hence (a "\/" b) = ( Top L) & (b "\/" a) = ( Top L) & (a "/\" b) = ( Bottom L) & (b "/\" a) = ( Bottom L) by A2, Th18, Th19;

      end;

      hence thesis;

    end;

    theorem :: SHEFFER1:24

    

     Th24: for L be Boolean lower-bounded' upper-bounded' distributive' Lattice-like non empty LattStr holds L is complemented'

    proof

      let L be Boolean lower-bounded' upper-bounded' distributive' Lattice-like non empty LattStr;

      for b be Element of L holds ex a be Element of L st a is_a_complement'_of b

      proof

        let b be Element of L;

        consider a be Element of L such that

         A1: a is_a_complement_of b by LATTICES:def 19;

        take a;

        

         A2: (b "/\" a) = ( Bottom L) by A1;

        (b "\/" a) = ( Top L) by A1;

        hence (b "\/" a) = ( Top' L) & (a "\/" b) = ( Top' L) & (b "/\" a) = ( Bot' L) & (a "/\" b) = ( Bot' L) by A2, Th20, Th21;

      end;

      hence thesis;

    end;

    theorem :: SHEFFER1:25

    

     Th25: for L be non empty LattStr holds L is Boolean Lattice iff L is lower-bounded' upper-bounded' join-commutative meet-commutative distributive distributive' complemented'

    proof

      let L be non empty LattStr;

      thus L is Boolean Lattice implies L is lower-bounded' upper-bounded' join-commutative meet-commutative distributive distributive' complemented'

      proof

        assume

         A1: L is Boolean Lattice;

        then

        reconsider L9 = L as Boolean Lattice;

        ex c be Element of L9 st for a be Element of L9 holds (c "\/" a) = a & (a "\/" c) = a

        proof

          take ( Bottom L9);

          thus thesis;

        end;

        hence

         A2: L is lower-bounded';

        ex c be Element of L9 st for a be Element of L9 holds (c "/\" a) = a & (a "/\" c) = a

        proof

          take ( Top L9);

          thus thesis;

        end;

        hence

         A3: L is upper-bounded';

        thus L is join-commutative meet-commutative by A1;

        for a,b,c be Element of L9 holds (a "/\" (b "\/" c)) = ((a "/\" b) "\/" (a "/\" c)) by LATTICES:def 11;

        then for a,b,c be Element of L9 holds (a "\/" (b "/\" c)) = ((a "\/" b) "/\" (a "\/" c)) by LATTICES: 3;

        hence L is distributive distributive';

        hence thesis by A1, A2, A3, Th24;

      end;

      thus L is lower-bounded' upper-bounded' join-commutative meet-commutative distributive distributive' complemented' implies L is Boolean Lattice

      proof

        assume L is lower-bounded' upper-bounded' join-commutative meet-commutative distributive distributive' complemented';

        then

        reconsider L9 = L as lower-bounded' upper-bounded' complemented' join-commutative meet-commutative join-idempotent distributive distributive' non empty LattStr by Th9;

        

         A4: L9 is complemented by Th23;

        

         A5: L9 is lower-bounded & L9 is upper-bounded by Th12, Th14;

        

         A6: L9 is meet-absorbing join-absorbing by Th10, Th11;

        then L9 is join-associative & L9 is meet-associative by Th16, Th17;

        hence thesis by A5, A4, A6;

      end;

    end;

    registration

      cluster Boolean Lattice-like -> lower-bounded' upper-bounded' complemented' join-commutative meet-commutative distributive distributive' for non empty LattStr;

      coherence by Th25;

      cluster lower-bounded' upper-bounded' complemented' join-commutative meet-commutative distributive distributive' -> Boolean Lattice-like for non empty LattStr;

      coherence by Th25;

    end

    begin

    definition

      struct ( 1-sorted) ShefferStr (# the carrier -> set,

the stroke -> BinOp of the carrier #)

       attr strict strict;

    end

    definition

      struct ( ShefferStr, LattStr) ShefferLattStr (# the carrier -> set,

the L_join -> BinOp of the carrier,

the L_meet -> BinOp of the carrier,

the stroke -> BinOp of the carrier #)

       attr strict strict;

    end

    definition

      struct ( ShefferStr, OrthoLattStr) ShefferOrthoLattStr (# the carrier -> set,

the L_join -> BinOp of the carrier,

the L_meet -> BinOp of the carrier,

the Compl -> UnOp of the carrier,

the stroke -> BinOp of the carrier #)

       attr strict strict;

    end

    definition

      :: SHEFFER1:def10

      func TrivShefferOrthoLattStr -> ShefferOrthoLattStr equals ShefferOrthoLattStr (# { 0 }, op2 , op2 , op1 , op2 #);

      coherence ;

    end

    registration

      cluster 1 -element for ShefferStr;

      existence

      proof

        set S = { {} };

        set B = the BinOp of S;

        take ShefferStr (# S, B #);

        thus the carrier of ShefferStr (# S, B #) is 1 -element;

      end;

      cluster 1 -element for ShefferLattStr;

      existence

      proof

        set S = { {} };

        set B = the BinOp of S;

        take ShefferLattStr (# S, B, B, B #);

        thus the carrier of ShefferLattStr (# S, B, B, B #) is 1 -element;

      end;

      cluster 1 -element for ShefferOrthoLattStr;

      existence

      proof

        set S = { {} };

        set B = the BinOp of S;

        set A = the UnOp of S;

        take ShefferOrthoLattStr (# S, B, B, A, B #);

        thus the carrier of ShefferOrthoLattStr (# S, B, B, A, B #) is 1 -element;

      end;

    end

    definition

      let L be non empty ShefferStr;

      let x,y be Element of L;

      :: SHEFFER1:def11

      func x | y -> Element of L equals (the stroke of L . (x,y));

      coherence ;

    end

    definition

      let L be non empty ShefferOrthoLattStr;

      :: SHEFFER1:def12

      attr L is properly_defined means

      : Def12: (for x be Element of L holds (x | x) = (x ` )) & (for x,y be Element of L holds (x "\/" y) = ((x | x) | (y | y))) & (for x,y be Element of L holds (x "/\" y) = ((x | y) | (x | y))) & for x,y be Element of L holds (x | y) = ((x ` ) + (y ` ));

    end

    definition

      let L be non empty ShefferStr;

      :: SHEFFER1:def13

      attr L is satisfying_Sheffer_1 means

      : Def13: for x be Element of L holds ((x | x) | (x | x)) = x;

      :: SHEFFER1:def14

      attr L is satisfying_Sheffer_2 means

      : Def14: for x,y be Element of L holds (x | (y | (y | y))) = (x | x);

      :: SHEFFER1:def15

      attr L is satisfying_Sheffer_3 means

      : Def15: for x,y,z be Element of L holds ((x | (y | z)) | (x | (y | z))) = (((y | y) | x) | ((z | z) | x));

    end

    registration

      cluster -> satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 for 1 -element ShefferStr;

      coherence by STRUCT_0:def 10;

    end

    registration

      cluster -> join-commutative join-associative for 1 -element \/-SemiLattStr;

      coherence by STRUCT_0:def 10;

      cluster -> meet-commutative meet-associative for 1 -element /\-SemiLattStr;

      coherence by STRUCT_0:def 10;

    end

    registration

      cluster -> join-absorbing meet-absorbing Boolean for 1 -element LattStr;

      coherence

      proof

        let L be 1 -element LattStr;

        thus L is join-absorbing by STRUCT_0:def 10;

        

         A1: L is upper-bounded

        proof

          set c = the Element of L;

          take c;

          let a be Element of L;

          thus thesis by STRUCT_0:def 10;

        end;

        thus L is meet-absorbing by STRUCT_0:def 10;

        

         A2: L is lower-bounded

        proof

          set c = the Element of L;

          take c;

          let a be Element of L;

          thus thesis by STRUCT_0:def 10;

        end;

        

         A3: L is complemented

        proof

          set a = the Element of L;

          let b be Element of L;

          take a;

          

           A4: (a "/\" b) = ( Bottom L) & (b "/\" a) = ( Bottom L) by STRUCT_0:def 10;

          (a "\/" b) = ( Top L) & (b "\/" a) = ( Top L) by STRUCT_0:def 10;

          hence thesis by A4;

        end;

        L is distributive by STRUCT_0:def 10;

        hence thesis by A2, A1, A3;

      end;

    end

    registration

      cluster TrivShefferOrthoLattStr -> 1 -element;

      coherence ;

      cluster TrivShefferOrthoLattStr -> properly_defined well-complemented;

      coherence

      proof

        set L = TrivShefferOrthoLattStr ;

        

         A1: (for x,y be Element of L holds (x "/\" y) = ((x | y) | (x | y))) & for x,y be Element of L holds (x | y) = ((x ` ) + (y ` )) by STRUCT_0:def 10;

        (for x be Element of L holds (x | x) = (x ` )) & for x,y be Element of L holds (x "\/" y) = ((x | x) | (y | y)) by STRUCT_0:def 10;

        hence L is properly_defined by A1;

        L is well-complemented

        proof

          let a be Element of L;

          thus ((a ` ) "\/" a) = ( Top L) & (a "\/" (a ` )) = ( Top L) & ((a ` ) "/\" a) = ( Bottom L) & (a "/\" (a ` )) = ( Bottom L) by STRUCT_0:def 10;

        end;

        hence thesis;

      end;

    end

    registration

      cluster properly_defined Boolean well-complemented Lattice-like satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 for non empty ShefferOrthoLattStr;

      existence

      proof

        take TrivShefferOrthoLattStr ;

        thus thesis;

      end;

    end

    theorem :: SHEFFER1:26

    for L be properly_defined Boolean well-complemented Lattice-like non empty ShefferOrthoLattStr holds L is satisfying_Sheffer_1

    proof

      let L be properly_defined Boolean well-complemented Lattice-like non empty ShefferOrthoLattStr;

      let x be Element of L;

      ((x ` ) ` ) = x by ROBBINS1: 3;

      then ((x | x) ` ) = x by Def12;

      hence thesis by Def12;

    end;

    theorem :: SHEFFER1:27

    for L be properly_defined Boolean well-complemented Lattice-like non empty ShefferOrthoLattStr holds L is satisfying_Sheffer_2

    proof

      let L be properly_defined Boolean well-complemented Lattice-like non empty ShefferOrthoLattStr;

      let x,y be Element of L;

      ((x ` ) + ( Bot L)) = (x ` ) by ROBBINS1: 13;

      then ((x ` ) + (((y ` ) ` ) *' (y ` ))) = (x ` ) by ROBBINS1: 15;

      then ((x ` ) + (((y ` ) + y) ` )) = (x ` ) by Th1;

      then (x | ((y ` ) + y)) = (x ` ) by Def12;

      then (x | ((y ` ) + ((y ` ) ` ))) = (x ` ) by ROBBINS1: 3;

      then (x | (y | (y ` ))) = (x ` ) by Def12;

      

      then (x | (y | (y | y))) = (x ` ) by Def12

      .= (x | x) by Def12;

      hence thesis;

    end;

    theorem :: SHEFFER1:28

    for L be properly_defined Boolean well-complemented Lattice-like non empty ShefferOrthoLattStr holds L is satisfying_Sheffer_3

    proof

      let L be properly_defined Boolean well-complemented Lattice-like non empty ShefferOrthoLattStr;

      let x,y,z be Element of L;

      (x *' ((y ` ) + (z ` ))) = (((y ` ) *' x) + ((z ` ) *' x)) by ROBBINS1: 30;

      then (((x ` ) + ((y | z) ` )) ` ) = (((y ` ) *' x) + ((z ` ) *' x)) by Def12;

      then ((x | (y | z)) ` ) = (((y ` ) *' x) + ((z ` ) *' x)) by Def12;

      

      then ((x | (y | z)) | (x | (y | z))) = (((y ` ) *' x) + ((z ` ) *' x)) by Def12

      .= (((y ` ) *' ((x ` ) ` )) + ((z ` ) *' x)) by ROBBINS1: 3

      .= (((y ` ) *' ((x ` ) ` )) + ((z ` ) *' ((x ` ) ` ))) by ROBBINS1: 3

      .= (((y + (x ` )) ` ) + ((z ` ) *' ((x ` ) ` ))) by Th1

      .= (((y + (x ` )) ` ) + ((z + (x ` )) ` )) by Th1

      .= ((y + (x ` )) | (z + (x ` ))) by Def12

      .= ((((y ` ) ` ) + (x ` )) | (z + (x ` ))) by ROBBINS1: 3

      .= ((((y ` ) ` ) + (x ` )) | (((z ` ) ` ) + (x ` ))) by ROBBINS1: 3

      .= (((y ` ) | x) | (((z ` ) ` ) + (x ` ))) by Def12

      .= (((y ` ) | x) | ((z ` ) | x)) by Def12

      .= (((y | y) | x) | ((z ` ) | x)) by Def12

      .= (((y | y) | x) | ((z | z) | x)) by Def12;

      hence thesis;

    end;

    definition

      let L be non empty ShefferStr;

      let a be Element of L;

      :: SHEFFER1:def16

      func a " -> Element of L equals (a | a);

      coherence ;

    end

    theorem :: SHEFFER1:29

    for L be satisfying_Sheffer_3 non empty ShefferOrthoLattStr, x,y,z be Element of L holds ((x | (y | z)) " ) = (((y " ) | x) | ((z " ) | x)) by Def15;

    theorem :: SHEFFER1:30

    for L be satisfying_Sheffer_1 non empty ShefferOrthoLattStr, x be Element of L holds x = ((x " ) " ) by Def13;

    theorem :: SHEFFER1:31

    

     Th31: for L be satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr, x,y be Element of L holds (x | y) = (y | x)

    proof

      let L be satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr;

      let x,y be Element of L;

      (x | y) = (((x | y) " ) " ) by Def13

      .= (((x | ((y " ) " )) " ) " ) by Def13

      .= (((((y " ) " ) | x) " ) " ) by Def15

      .= (((y | x) " ) " ) by Def13

      .= (y | x) by Def13;

      hence thesis;

    end;

    theorem :: SHEFFER1:32

    

     Th32: for L be satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr, x,y be Element of L holds (x | (x | x)) = (y | (y | y))

    proof

      let L be satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr;

      let x,y be Element of L;

      (x | (x | x)) = (((x | (x " )) | (x | (x " ))) " ) by Def13

      .= (((x | (x " )) | (y | (y " ))) " ) by Def14

      .= (((y | (y " )) | (x | (x | x))) " ) by Th31

      .= (((y | (y " )) " ) " ) by Def14

      .= (y | (y | y)) by Def13;

      hence thesis;

    end;

    theorem :: SHEFFER1:33

    

     Th33: for L be satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr holds L is join-commutative

    proof

      let L be satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr;

      let x,y be Element of L;

      (x "\/" y) = ((x " ) | (y | y)) by Def12

      .= ((y | y) | (x | x)) by Th31

      .= (y "\/" x) by Def12;

      hence thesis;

    end;

    theorem :: SHEFFER1:34

    

     Th34: for L be satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr holds L is meet-commutative

    proof

      let L be satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr;

      let x,y be Element of L;

      (x "/\" y) = ((x | y) | (x | y)) by Def12

      .= ((y | x) | (x | y)) by Th31

      .= ((y | x) | (y | x)) by Th31

      .= (y "/\" x) by Def12;

      hence thesis;

    end;

    theorem :: SHEFFER1:35

    

     Th35: for L be satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr holds L is distributive

    proof

      let L be satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr;

      let x,y,z be Element of L;

      set Y = (y " );

      set Z = (z " );

      (x "/\" (y "\/" z)) = (x "/\" ((y | y) | (z | z))) by Def12

      .= ((x | (Y | Z)) " ) by Def12

      .= (((Y " ) | x) | ((Z " ) | x)) by Def15

      .= ((y | x) | ((Z " ) | x)) by Def13

      .= ((y | x) | (z | x)) by Def13

      .= ((x | y) | (z | x)) by Th31

      .= ((x | y) | (x | z)) by Th31

      .= ((((x | y) " ) " ) | (x | z)) by Def13

      .= ((((x | y) | (x | y)) " ) | (((x | z) " ) " )) by Def13

      .= (((x "/\" y) | ((x | y) | (x | y))) | (((x | z) | (x | z)) | ((x | z) | (x | z)))) by Def12

      .= (((x "/\" y) | (x "/\" y)) | (((x | z) | (x | z)) | ((x | z) | (x | z)))) by Def12

      .= (((x "/\" y) | (x "/\" y)) | ((x "/\" z) | ((x | z) | (x | z)))) by Def12

      .= (((x "/\" y) | (x "/\" y)) | ((x "/\" z) | (x "/\" z))) by Def12

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

      hence thesis;

    end;

    theorem :: SHEFFER1:36

    

     Th36: for L be satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr holds L is distributive'

    proof

      let L be satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr;

      let x,y,z be Element of L;

      set X = (x | x);

      (x "\/" (y "/\" z)) = (x "\/" ((y | z) | (y | z))) by Def12

      .= (X | (((y | z) " ) " )) by Def12

      .= (X | (y | z)) by Def13

      .= (((X | (y | z)) " ) " ) by Def13

      .= ((((y " ) | X) | ((z " ) | X)) " ) by Def15

      .= (((X | (y " )) | ((z " ) | X)) " ) by Th31

      .= (((X | (y | y)) | (X | (z " ))) " ) by Th31

      .= (((x "\/" y) | (X | (z | z))) | ((X | (y | y)) | (X | (z | z)))) by Def12

      .= (((x "\/" y) | (x "\/" z)) | ((X | (y | y)) | (X | (z | z)))) by Def12

      .= (((x "\/" y) | (x "\/" z)) | ((x "\/" y) | (X | (z | z)))) by Def12

      .= (((x "\/" y) | (x "\/" z)) | ((x "\/" y) | (x "\/" z))) by Def12

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

      hence thesis;

    end;

    theorem :: SHEFFER1:37

    for L be satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr holds L is Boolean Lattice

    proof

      let L be satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 properly_defined non empty ShefferOrthoLattStr;

      

       A1: L is distributive & L is distributive' by Th35, Th36;

      ex c be Element of L st for a be Element of L holds (c "/\" a) = a & (a "/\" c) = a

      proof

        set b = the Element of L;

        take c = ((b | b) | ((b | b) | (b | b)));

        let a be Element of L;

        thus (c "/\" a) = a

        proof

          set X = (b " );

          (c "/\" a) = ((((b | b) | (X | X)) | a) " ) by Def12

          .= ((a | (X | (X | X))) " ) by Th31

          .= ((a | a) " ) by Def14

          .= a by Def13;

          hence thesis;

        end;

        thus (a "/\" c) = a

        proof

          set X = (b " );

          (a "/\" c) = ((a | ((b | b) | (X | X))) " ) by Def12

          .= ((a | a) " ) by Def14

          .= a by Def13;

          hence thesis;

        end;

      end;

      then

       A2: L is upper-bounded';

      ex c be Element of L st for a be Element of L holds (c "\/" a) = a & (a "\/" c) = a

      proof

        set b = the Element of L;

        take c = ((b | (b | b)) | (b | (b | b)));

        let a be Element of L;

        (c "\/" a) = ((((b | (b | b)) " ) " ) | (a | a)) by Def12

        .= ((((a | (a | a)) " ) " ) | (a | a)) by Th32

        .= ((a | (a | a)) | (a | a)) by Def13

        .= ((a | a) | (a | (a | a))) by Th31

        .= ((a | a) | (a | a)) by Def14

        .= a by Def13;

        hence (c "\/" a) = a;

        (a "\/" c) = ((a | a) | (((b | (b | b)) " ) " )) by Def12

        .= ((a | a) | (((a | (a | a)) " ) " )) by Th32

        .= ((a | a) | (a | (a | a))) by Def13

        .= ((a | a) | (a | a)) by Def14

        .= a by Def13;

        hence (a "\/" c) = a;

      end;

      then

       A3: L is lower-bounded';

      for b be Element of L holds ex a be Element of L st a is_a_complement'_of b

      proof

        let b be Element of L;

        set a = (b | b);

        take a;

        

         A4: ( Top' L) = ((b | b) | ((b | b) | (b | b)))

        proof

          set X = ((b | b) | ((b | b) | (b | b)));

          for a be Element of L holds (X "/\" a) = a & (a "/\" X) = a

          proof

            let a be Element of L;

            set Y = (b " );

            

            thus (X "/\" a) = ((((b | b) | (Y | Y)) | a) " ) by Def12

            .= ((a | (Y | (Y | Y))) " ) by Th31

            .= ((a | a) " ) by Def14

            .= a by Def13;

            

            thus (a "/\" X) = ((a | ((b | b) | (Y | Y))) " ) by Def12

            .= ((a | a) " ) by Def14

            .= a by Def13;

          end;

          hence thesis by A2, Def2;

        end;

        then

         A5: (b "\/" a) = ( Top' L) by Def12;

        

         A6: ( Bot' L) = ((b | (b | b)) | (b | (b | b)))

        proof

          set X = ((b | (b | b)) | (b | (b | b)));

          for a be Element of L holds (X "\/" a) = a & (a "\/" X) = a

          proof

            let a be Element of L;

            

            thus (X "\/" a) = ((((b | (b | b)) " ) " ) | (a | a)) by Def12

            .= ((((a | (a | a)) " ) " ) | (a | a)) by Th32

            .= ((a | (a | a)) | (a | a)) by Def13

            .= ((a | a) | (a | (a | a))) by Th31

            .= ((a | a) | (a | a)) by Def14

            .= a by Def13;

            

            thus (a "\/" X) = ((a | a) | (((b | (b | b)) " ) " )) by Def12

            .= ((a | a) | (((a | (a | a)) " ) " )) by Th32

            .= ((a | a) | (a | (a | a))) by Def13

            .= ((a | a) | (a | a)) by Def14

            .= a by Def13;

          end;

          hence thesis by A3, Def4;

        end;

        then

         A7: (b "/\" a) = ( Bot' L) by Def12;

        

         A8: (a "\/" b) = (((b | b) | (b | b)) | (b | b)) by Def12

        .= ( Top' L) by A4, Th31;

        (a "/\" b) = (((b | b) | b) | ((b | b) | b)) by Def12

        .= ((b | (b | b)) | ((b | b) | b)) by Th31

        .= ( Bot' L) by A6, Th31;

        hence thesis by A8, A5, A7;

      end;

      then

       A9: L is complemented';

      L is join-commutative & L is meet-commutative by Th33, Th34;

      hence thesis by A3, A2, A9, A1;

    end;