:: by Violetta Kozarkiewicz and Adam Grabowski

::

:: Received May 31, 2004

:: Copyright (c) 2004-2021 Association of Mizar Users

theorem Th1: :: SHEFFER1:1

for L being non empty join-commutative join-associative Huntington ComplLLattStr

for a, b being Element of L holds (a + b) ` = (a `) *' (b `)

for a, b being Element of L holds (a + b) ` = (a `) *' (b `)

proof end;

definition

let IT be non empty LattStr ;

end;
attr IT is upper-bounded' means :: SHEFFER1:def 1

ex c being Element of IT st

for a being Element of IT holds

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

ex c being Element of IT st

for a being Element of IT holds

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

:: deftheorem defines upper-bounded' SHEFFER1:def 1 :

for IT being non empty LattStr holds

( IT is upper-bounded' iff ex c being Element of IT st

for a being Element of IT holds

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

for IT being non empty LattStr holds

( IT is upper-bounded' iff ex c being Element of IT st

for a being Element of IT holds

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

definition

let L be non empty LattStr ;

assume A1: L is upper-bounded' ;

ex b_{1} being Element of L st

for a being Element of L holds

( b_{1} "/\" a = a & a "/\" b_{1} = a )
by A1;

uniqueness

for b_{1}, b_{2} being Element of L st ( for a being Element of L holds

( b_{1} "/\" a = a & a "/\" b_{1} = a ) ) & ( for a being Element of L holds

( b_{2} "/\" a = a & a "/\" b_{2} = a ) ) holds

b_{1} = b_{2}

end;
assume A1: L is upper-bounded' ;

func Top' L -> Element of L means :Def2: :: SHEFFER1:def 2

for a being Element of L holds

( it "/\" a = a & a "/\" it = a );

existence for a being Element of L holds

( it "/\" a = a & a "/\" it = a );

ex b

for a being Element of L holds

( b

uniqueness

for b

( b

( b

b

proof end;

:: deftheorem Def2 defines Top' SHEFFER1:def 2 :

for L being non empty LattStr st L is upper-bounded' holds

for b_{2} being Element of L holds

( b_{2} = Top' L iff for a being Element of L holds

( b_{2} "/\" a = a & a "/\" b_{2} = a ) );

for L being non empty LattStr st L is upper-bounded' holds

for b

( b

( b

definition

let IT be non empty LattStr ;

end;
attr IT is lower-bounded' means :: SHEFFER1:def 3

ex c being Element of IT st

for a being Element of IT holds

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

ex c being Element of IT st

for a being Element of IT holds

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

:: deftheorem defines lower-bounded' SHEFFER1:def 3 :

for IT being non empty LattStr holds

( IT is lower-bounded' iff ex c being Element of IT st

for a being Element of IT holds

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

for IT being non empty LattStr holds

( IT is lower-bounded' iff ex c being Element of IT st

for a being Element of IT holds

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

definition

let L be non empty LattStr ;

assume A1: L is lower-bounded' ;

ex b_{1} being Element of L st

for a being Element of L holds

( b_{1} "\/" a = a & a "\/" b_{1} = a )
by A1;

uniqueness

for b_{1}, b_{2} being Element of L st ( for a being Element of L holds

( b_{1} "\/" a = a & a "\/" b_{1} = a ) ) & ( for a being Element of L holds

( b_{2} "\/" a = a & a "\/" b_{2} = a ) ) holds

b_{1} = b_{2}

end;
assume A1: L is lower-bounded' ;

func Bot' L -> Element of L means :Def4: :: SHEFFER1:def 4

for a being Element of L holds

( it "\/" a = a & a "\/" it = a );

existence for a being Element of L holds

( it "\/" a = a & a "\/" it = a );

ex b

for a being Element of L holds

( b

uniqueness

for b

( b

( b

b

proof end;

:: deftheorem Def4 defines Bot' SHEFFER1:def 4 :

for L being non empty LattStr st L is lower-bounded' holds

for b_{2} being Element of L holds

( b_{2} = Bot' L iff for a being Element of L holds

( b_{2} "\/" a = a & a "\/" b_{2} = a ) );

for L being non empty LattStr st L is lower-bounded' holds

for b

( b

( b

definition

let IT be non empty LattStr ;

end;
attr IT is distributive' means :Def5: :: SHEFFER1:def 5

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

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

:: deftheorem Def5 defines distributive' SHEFFER1:def 5 :

for IT being non empty LattStr holds

( IT is distributive' iff for a, b, c being Element of IT holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) );

for IT being non empty LattStr holds

( IT is distributive' iff for a, b, c being Element of IT holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) );

:: deftheorem defines is_a_complement'_of SHEFFER1:def 6 :

for L being non empty LattStr

for a, b being Element of L holds

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

for L being non empty LattStr

for a, b being Element of L holds

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

definition

let IT be non empty LattStr ;

end;
attr IT is complemented' means :Def7: :: SHEFFER1:def 7

for b being Element of IT ex a being Element of IT st a is_a_complement'_of b;

for b being Element of IT ex a being Element of IT st a is_a_complement'_of b;

:: deftheorem Def7 defines complemented' SHEFFER1:def 7 :

for IT being non empty LattStr holds

( IT is complemented' iff for b being Element of IT ex a being Element of IT st a is_a_complement'_of b );

for IT being non empty LattStr holds

( IT is complemented' iff for b being Element of IT ex a being Element of IT st a is_a_complement'_of b );

definition

let L be non empty LattStr ;

let x be Element of L;

assume A1: ( L is complemented' & L is distributive & L is upper-bounded' & L is meet-commutative ) ;

existence

ex b_{1} being Element of L st b_{1} is_a_complement'_of x
by A1;

uniqueness

for b_{1}, b_{2} being Element of L st b_{1} is_a_complement'_of x & b_{2} is_a_complement'_of x holds

b_{1} = b_{2}

end;
let x be Element of L;

assume A1: ( L is complemented' & L is distributive & L is upper-bounded' & L is meet-commutative ) ;

existence

ex b

uniqueness

for b

b

proof end;

:: deftheorem Def8 defines `# SHEFFER1:def 8 :

for L being non empty LattStr

for x being Element of L st L is complemented' & L is distributive & L is upper-bounded' & L is meet-commutative holds

for b_{3} being Element of L holds

( b_{3} = x `# iff b_{3} is_a_complement'_of x );

for L being non empty LattStr

for x being Element of L st L is complemented' & L is distributive & L is upper-bounded' & L is meet-commutative holds

for b

( b

registration

ex b_{1} being 1 -element LattStr st

( b_{1} is Boolean & b_{1} is join-idempotent & b_{1} is upper-bounded' & b_{1} is complemented' & b_{1} is distributive' & b_{1} is lower-bounded' & b_{1} is Lattice-like )
end;

cluster non empty V48() V49() 1 -element Lattice-like Boolean join-idempotent upper-bounded' lower-bounded' distributive' complemented' for LattStr ;

existence ex b

( b

proof end;

theorem Th2: :: SHEFFER1:2

for L being non empty join-commutative meet-commutative distributive upper-bounded' distributive' complemented' LattStr

for x being Element of L holds x "\/" (x `#) = Top' L

for x being Element of L holds x "\/" (x `#) = Top' L

proof end;

theorem Th3: :: SHEFFER1:3

for L being non empty join-commutative meet-commutative distributive upper-bounded' distributive' complemented' LattStr

for x being Element of L holds x "/\" (x `#) = Bot' L

for x being Element of L holds x "/\" (x `#) = Bot' L

proof end;

theorem Th4: :: SHEFFER1:4

for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' distributive' complemented' LattStr

for x being Element of L holds x "\/" (Top' L) = Top' L

for x being Element of L holds x "\/" (Top' L) = Top' L

proof end;

theorem Th5: :: SHEFFER1:5

for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr

for x being Element of L holds x "/\" (Bot' L) = Bot' L

for x being Element of L holds x "/\" (Bot' L) = Bot' L

proof end;

theorem Th6: :: SHEFFER1:6

for L being non empty join-commutative meet-commutative meet-absorbing join-absorbing distributive join-idempotent LattStr

for x, y, z being Element of L holds ((x "\/" y) "\/" z) "/\" x = x

for x, y, z being Element of L holds ((x "\/" y) "\/" z) "/\" x = x

proof end;

theorem Th7: :: SHEFFER1:7

for L being non empty join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent distributive' LattStr

for x, y, z being Element of L holds ((x "/\" y) "/\" z) "\/" x = x

for x, y, z being Element of L holds ((x "/\" y) "/\" z) "\/" x = x

proof end;

:: deftheorem defines meet-idempotent SHEFFER1:def 9 :

for G being non empty /\-SemiLattStr holds

( G is meet-idempotent iff for x being Element of G holds x "/\" x = x );

for G being non empty /\-SemiLattStr holds

( G is meet-idempotent iff for x being Element of G holds x "/\" x = x );

theorem Th8: :: SHEFFER1:8

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

proof end;

theorem Th9: :: SHEFFER1:9

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

proof end;

theorem Th10: :: SHEFFER1:10

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

proof end;

theorem Th11: :: SHEFFER1:11

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

proof end;

theorem Th12: :: SHEFFER1:12

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

proof end;

theorem Th14: :: SHEFFER1:14

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

proof end;

theorem Th16: :: SHEFFER1:16

for L being non empty join-commutative meet-commutative meet-absorbing join-absorbing distributive join-idempotent LattStr holds L is join-associative

proof end;

theorem Th17: :: SHEFFER1:17

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

proof end;

theorem Th18: :: SHEFFER1:18

for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr holds Top L = Top' L

proof end;

theorem Th19: :: SHEFFER1:19

for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr holds Bottom L = Bot' L

proof end;

theorem Th21: :: SHEFFER1:21

for L being non empty Lattice-like distributive lower-bounded upper-bounded complemented Boolean distributive' LattStr holds Bottom L = Bot' L

proof end;

theorem :: SHEFFER1:22

for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr

for x, y being Element of L holds

( x is_a_complement'_of y iff x is_a_complement_of y ) by Th19, Th18;

for x, y being Element of L holds

( x is_a_complement'_of y iff x is_a_complement_of y ) by Th19, Th18;

theorem Th23: :: SHEFFER1:23

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

proof end;

theorem Th24: :: SHEFFER1:24

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

proof end;

theorem Th25: :: SHEFFER1:25

for L being non empty LattStr holds

( L is Boolean Lattice iff ( L is lower-bounded' & L is upper-bounded' & L is join-commutative & L is meet-commutative & L is distributive & L is distributive' & L is complemented' ) )

( L is Boolean Lattice iff ( L is lower-bounded' & L is upper-bounded' & L is join-commutative & L is meet-commutative & L is distributive & L is distributive' & L is complemented' ) )

proof end;

registration

for b_{1} being non empty LattStr st b_{1} is Boolean & b_{1} is Lattice-like holds

( b_{1} is lower-bounded' & b_{1} is upper-bounded' & b_{1} is complemented' & b_{1} is join-commutative & b_{1} is meet-commutative & b_{1} is distributive & b_{1} is distributive' )
by Th25;

for b_{1} being non empty LattStr st b_{1} is lower-bounded' & b_{1} is upper-bounded' & b_{1} is complemented' & b_{1} is join-commutative & b_{1} is meet-commutative & b_{1} is distributive & b_{1} is distributive' holds

( b_{1} is Boolean & b_{1} is Lattice-like )
by Th25;

end;

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

coherence for b

( b

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

coherence for b

( b

definition

attr c_{1} is strict ;

struct ShefferStr -> 1-sorted ;

aggr ShefferStr(# carrier, stroke #) -> ShefferStr ;

sel stroke c_{1} -> BinOp of the carrier of c_{1};

end;
struct ShefferStr -> 1-sorted ;

aggr ShefferStr(# carrier, stroke #) -> ShefferStr ;

sel stroke c

definition

attr c_{1} is strict ;

struct ShefferLattStr -> ShefferStr , LattStr ;

aggr ShefferLattStr(# carrier, L_join, L_meet, stroke #) -> ShefferLattStr ;

end;
struct ShefferLattStr -> ShefferStr , LattStr ;

aggr ShefferLattStr(# carrier, L_join, L_meet, stroke #) -> ShefferLattStr ;

definition

attr c_{1} is strict ;

struct ShefferOrthoLattStr -> ShefferStr , OrthoLattStr ;

aggr ShefferOrthoLattStr(# carrier, L_join, L_meet, Compl, stroke #) -> ShefferOrthoLattStr ;

end;
struct ShefferOrthoLattStr -> ShefferStr , OrthoLattStr ;

aggr ShefferOrthoLattStr(# carrier, L_join, L_meet, Compl, stroke #) -> ShefferOrthoLattStr ;

definition

ShefferOrthoLattStr(# {0},op2,op2,op1,op2 #) is ShefferOrthoLattStr ;

end;

func TrivShefferOrthoLattStr -> ShefferOrthoLattStr equals :: SHEFFER1:def 10

ShefferOrthoLattStr(# {0},op2,op2,op1,op2 #);

coherence ShefferOrthoLattStr(# {0},op2,op2,op1,op2 #);

ShefferOrthoLattStr(# {0},op2,op2,op1,op2 #) is ShefferOrthoLattStr ;

:: deftheorem defines TrivShefferOrthoLattStr SHEFFER1:def 10 :

TrivShefferOrthoLattStr = ShefferOrthoLattStr(# {0},op2,op2,op1,op2 #);

TrivShefferOrthoLattStr = ShefferOrthoLattStr(# {0},op2,op2,op1,op2 #);

registration

existence

ex b_{1} being ShefferStr st b_{1} is 1 -element

ex b_{1} being ShefferLattStr st b_{1} is 1 -element

ex b_{1} being ShefferOrthoLattStr st b_{1} is 1 -element

end;
ex b

proof end;

existence ex b

proof end;

existence ex b

proof end;

definition

let L be non empty ShefferStr ;

let x, y be Element of L;

coherence

the stroke of L . (x,y) is Element of L ;

end;
let x, y be Element of L;

coherence

the stroke of L . (x,y) is Element of L ;

:: deftheorem defines | SHEFFER1:def 11 :

for L being non empty ShefferStr

for x, y being Element of L holds x | y = the stroke of L . (x,y);

for L being non empty ShefferStr

for x, y being Element of L holds x | y = the stroke of L . (x,y);

definition

let L be non empty ShefferOrthoLattStr ;

end;
attr L is properly_defined means :Def12: :: SHEFFER1:def 12

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

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

:: deftheorem Def12 defines properly_defined SHEFFER1:def 12 :

for L being non empty ShefferOrthoLattStr holds

( L is properly_defined iff ( ( for x being Element of L holds x | x = x ` ) & ( for x, y being Element of L holds x "\/" y = (x | x) | (y | y) ) & ( for x, y being Element of L holds x "/\" y = (x | y) | (x | y) ) & ( for x, y being Element of L holds x | y = (x `) + (y `) ) ) );

for L being non empty ShefferOrthoLattStr holds

( L is properly_defined iff ( ( for x being Element of L holds x | x = x ` ) & ( for x, y being Element of L holds x "\/" y = (x | x) | (y | y) ) & ( for x, y being Element of L holds x "/\" y = (x | y) | (x | y) ) & ( for x, y being Element of L holds x | y = (x `) + (y `) ) ) );

definition

let L be non empty ShefferStr ;

end;
attr L is satisfying_Sheffer_1 means :Def13: :: SHEFFER1:def 13

for x being Element of L holds (x | x) | (x | x) = x;

for x being Element of L holds (x | x) | (x | x) = x;

attr L is satisfying_Sheffer_2 means :Def14: :: SHEFFER1:def 14

for x, y being Element of L holds x | (y | (y | y)) = x | x;

for x, y being Element of L holds x | (y | (y | y)) = x | x;

:: deftheorem Def13 defines satisfying_Sheffer_1 SHEFFER1:def 13 :

for L being non empty ShefferStr holds

( L is satisfying_Sheffer_1 iff for x being Element of L holds (x | x) | (x | x) = x );

for L being non empty ShefferStr holds

( L is satisfying_Sheffer_1 iff for x being Element of L holds (x | x) | (x | x) = x );

:: deftheorem Def14 defines satisfying_Sheffer_2 SHEFFER1:def 14 :

for L being non empty ShefferStr holds

( L is satisfying_Sheffer_2 iff for x, y being Element of L holds x | (y | (y | y)) = x | x );

for L being non empty ShefferStr holds

( L is satisfying_Sheffer_2 iff for x, y being Element of L holds x | (y | (y | y)) = x | x );

:: deftheorem Def15 defines satisfying_Sheffer_3 SHEFFER1:def 15 :

for L being non empty ShefferStr holds

( L is satisfying_Sheffer_3 iff for x, y, z being Element of L holds (x | (y | z)) | (x | (y | z)) = ((y | y) | x) | ((z | z) | x) );

for L being non empty ShefferStr holds

( L is satisfying_Sheffer_3 iff for x, y, z being Element of L holds (x | (y | z)) | (x | (y | z)) = ((y | y) | x) | ((z | z) | x) );

registration

for b_{1} being 1 -element ShefferStr holds

( b_{1} is satisfying_Sheffer_1 & b_{1} is satisfying_Sheffer_2 & b_{1} is satisfying_Sheffer_3 )
by STRUCT_0:def 10;

end;

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

coherence for b

( b

registration

coherence

for b_{1} being 1 -element \/-SemiLattStr holds

( b_{1} is join-commutative & b_{1} is join-associative )
by STRUCT_0:def 10;

coherence

for b_{1} being 1 -element /\-SemiLattStr holds

( b_{1} is meet-commutative & b_{1} is meet-associative )
by STRUCT_0:def 10;

end;
for b

( b

coherence

for b

( b

registration

coherence

for b_{1} being 1 -element LattStr holds

( b_{1} is join-absorbing & b_{1} is meet-absorbing & b_{1} is Boolean )

end;
for b

( b

proof end;

registration

coherence

TrivShefferOrthoLattStr is 1 -element ;

coherence

( TrivShefferOrthoLattStr is properly_defined & TrivShefferOrthoLattStr is well-complemented )

end;
TrivShefferOrthoLattStr is 1 -element ;

coherence

( TrivShefferOrthoLattStr is properly_defined & TrivShefferOrthoLattStr is well-complemented )

proof end;

registration

ex b_{1} being non empty ShefferOrthoLattStr st

( b_{1} is properly_defined & b_{1} is Boolean & b_{1} is well-complemented & b_{1} is Lattice-like & b_{1} is satisfying_Sheffer_1 & b_{1} is satisfying_Sheffer_2 & b_{1} is satisfying_Sheffer_3 )
end;

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

existence ex b

( b

proof end;

theorem :: SHEFFER1:26

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

proof end;

theorem :: SHEFFER1:27

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

proof end;

theorem :: SHEFFER1:28

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

proof end;

definition
end;

:: deftheorem defines " SHEFFER1:def 16 :

for L being non empty ShefferStr

for a being Element of L holds a " = a | a;

for L being non empty ShefferStr

for a being Element of L holds a " = a | a;

theorem :: SHEFFER1:29

theorem :: SHEFFER1:30

for L being non empty satisfying_Sheffer_1 ShefferOrthoLattStr

for x being Element of L holds x = (x ") " by Def13;

for x being Element of L holds x = (x ") " by Def13;

theorem Th31: :: SHEFFER1:31

for L being non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr

for x, y being Element of L holds x | y = y | x

for x, y being Element of L holds x | y = y | x

proof end;

theorem Th32: :: SHEFFER1:32

for L being non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr

for x, y being Element of L holds x | (x | x) = y | (y | y)

for x, y being Element of L holds x | (x | x) = y | (y | y)

proof end;

theorem Th33: :: SHEFFER1:33

for L being non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr holds L is join-commutative

proof end;

theorem Th34: :: SHEFFER1:34

for L being non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr holds L is meet-commutative

proof end;

theorem Th35: :: SHEFFER1:35

for L being non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr holds L is distributive

proof end;

theorem Th36: :: SHEFFER1:36

for L being non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr holds L is distributive'

proof end;

theorem :: SHEFFER1:37

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

proof end;