:: SHEFFER1 semantic presentation

begin

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 `)
proof
let L be non empty join-commutative join-associative Huntington ComplLLattStr ; ::_thesis: for a, b being Element of L holds (a + b) ` = (a `) *' (b `)
let a, b be Element of L; ::_thesis: (a + b) ` = (a `) *' (b `)
 a + b = ((a `) *' (b `)) ` by ROBBINS1:17;
hence  (a + b) ` = (a `) *' (b `) by ROBBINS1:3; ::_thesis: verum
end;

begin

definition
let IT be non empty LattStr ;
attrIT is upper-bounded'  means :Def1: :: SHEFFER1:def 1
 ex c being Element of IT st
for a being Element of IT holds
( c "/\" a = a & a "/\" c = a );
end;

:: deftheorem Def1 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 ) );

definition
let L be non empty LattStr ;
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
 ex b1 being Element of L st
for a being Element of L holds
( b1 "/\" a = a & a "/\" b1 = a ) by A1, Def1;
uniqueness
 for b1, b2 being Element of L st ( for a being Element of L holds
( b1 "/\" a = a & a "/\" b1 = a ) ) & ( for a being Element of L holds
( b2 "/\" a = a & a "/\" b2 = a ) ) holds
b1 = b2
proof
let c1, c2 be Element of L; ::_thesis: ( ( for a being Element of L holds
( c1 "/\" a = a & a "/\" c1 = a ) ) & ( for a being Element of L holds
( c2 "/\" a = a & a "/\" c2 = a ) ) implies c1 = c2 )
assume that
A2: for a being Element of L holds
( c1 "/\" a = a & a "/\" c1 = a ) and
A3: for a being Element of L holds
( c2 "/\" a = a & a "/\" c2 = a ) ; ::_thesis: c1 = c2
thus c1 = c2 "/\" c1 by A3
.= c2 by A2 ; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines Top' SHEFFER1:def_2_:_
 for L being non empty LattStr st L is upper-bounded' holds
for b2 being Element of L holds
( b2 = Top' L iff for a being Element of L holds
( b2 "/\" a = a & a "/\" b2 = a ) );

definition
let IT be non empty LattStr ;
attrIT is lower-bounded'  means :Def3: :: SHEFFER1:def 3
 ex c being Element of IT st
for a being Element of IT holds
( c "\/" a = a & a "\/" c = a );
end;

:: deftheorem Def3 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 ) );

definition
let L be non empty LattStr ;
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
 ex b1 being Element of L st
for a being Element of L holds
( b1 "\/" a = a & a "\/" b1 = a ) by A1, Def3;
uniqueness
 for b1, b2 being Element of L st ( for a being Element of L holds
( b1 "\/" a = a & a "\/" b1 = a ) ) & ( for a being Element of L holds
( b2 "\/" a = a & a "\/" b2 = a ) ) holds
b1 = b2
proof
let c1, c2 be Element of L; ::_thesis: ( ( for a being Element of L holds
( c1 "\/" a = a & a "\/" c1 = a ) ) & ( for a being Element of L holds
( c2 "\/" a = a & a "\/" c2 = a ) ) implies c1 = c2 )
assume that
A2: for a being Element of L holds
( c1 "\/" a = a & a "\/" c1 = a ) and
A3: for a being Element of L holds
( c2 "\/" a = a & a "\/" c2 = a ) ; ::_thesis: c1 = c2
thus c1 = c2 "\/" c1 by A3
.= c2 by A2 ; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines Bot' SHEFFER1:def_4_:_
 for L being non empty LattStr st L is lower-bounded' holds
for b2 being Element of L holds
( b2 = Bot' L iff for a being Element of L holds
( b2 "\/" a = a & a "\/" b2 = a ) );

definition
let IT be non empty LattStr ;
attrIT is distributive'  means :Def5: :: SHEFFER1:def 5
 for a, b, c being Element of IT holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c);
end;

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

definition
let L be non empty LattStr ;
let a, b be Element of L;
preda is_a_complement'_of b means :Def6: :: SHEFFER1:def 6
( b "\/" a = Top' L & a "\/" b = Top' L & b "/\" a = Bot' L & a "/\" b = Bot' L );
end;

:: deftheorem Def6 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 ) );

definition
let IT be non empty LattStr ;
attrIT 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;
end;

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

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 ) ;
funcx `#  ->  Element of L means :Def8: :: SHEFFER1:def 8
it is_a_complement'_of x;
existence
 ex b1 being Element of L st b1 is_a_complement'_of x by A1, Def7;
uniqueness
 for b1, b2 being Element of L st b1 is_a_complement'_of x & b2 is_a_complement'_of x holds
b1 = b2
proof
let a, b be Element of L; ::_thesis: ( a is_a_complement'_of x & b is_a_complement'_of x implies a = b )
assume that
A2: a is_a_complement'_of x and
A3: b is_a_complement'_of x ; ::_thesis: a = b
b = b "/\" (Top' L) by A1, Def2
.= b "/\" (x "\/" a) by A2, Def6
.= (b "/\" x) "\/" (b "/\" a) by A1, LATTICES:def_11
.= (x "/\" b) "\/" (b "/\" a) by A1, LATTICES:def_6
.= (x "/\" b) "\/" (a "/\" b) by A1, LATTICES:def_6
.= (Bot' L) "\/" (a "/\" b) by A3, Def6
.= (a "/\" x) "\/" (a "/\" b) by A2, Def6
.= a "/\" (x "\/" b) by A1, LATTICES:def_11
.= a "/\" (Top' L) by A3, Def6
.= a by A1, Def2 ;
hence  a = b ; ::_thesis: verum
end;
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 b3 being Element of L holds
( b3 = x `# iff b3 is_a_complement'_of x );

registration
cluster non empty V45() V46() 1 -element Lattice-like Boolean join-idempotent upper-bounded' lower-bounded' distributive' complemented' for LattStr ;
existence
 ex b1 being 1 -element LattStr st
( b1 is Boolean & b1 is join-idempotent & b1 is upper-bounded' & b1 is complemented' & b1 is distributive' & b1 is lower-bounded' & b1 is Lattice-like )
proof
set L = the 1 -element Lattice;
A1: the 1 -element Lattice is lower-bounded
proof
set x = the Element of the 1 -element Lattice;
 for y being Element of the 1 -element Lattice holds
( the Element of the 1 -element Lattice "/\" y = the Element of the 1 -element Lattice & y "/\" the Element of the 1 -element Lattice = the Element of the 1 -element Lattice ) by STRUCT_0:def_10;
hence  the 1 -element Lattice is lower-bounded by LATTICES:def_13; ::_thesis: verum
end;
A2: the 1 -element Lattice is upper-bounded
proof
set x = the Element of the 1 -element Lattice;
 for y being Element of the 1 -element Lattice holds
( the Element of the 1 -element Lattice "\/" y = the Element of the 1 -element Lattice & y "\/" the Element of the 1 -element Lattice = the Element of the 1 -element Lattice ) by STRUCT_0:def_10;
hence  the 1 -element Lattice is upper-bounded by LATTICES:def_14; ::_thesis: verum
end;
 for b being Element of the 1 -element Lattice ex a being Element of the 1 -element Lattice st a is_a_complement_of b
proof
let b be Element of the 1 -element Lattice; ::_thesis: ex a being Element of the 1 -element Lattice st a is_a_complement_of b
take a = b; ::_thesis: a is_a_complement_of b
 ( b "\/" a = Top the 1 -element Lattice & b "/\" a = Bottom the 1 -element Lattice ) by STRUCT_0:def_10;
hence  a is_a_complement_of b by LATTICES:def_18; ::_thesis: verum
end;
then A3: the 1 -element Lattice is complemented by LATTICES:def_19;
A4: the 1 -element Lattice is join-idempotent
proof
let x be Element of the 1 -element Lattice; :: according to ROBBINS1:def_7 ::_thesis: x "\/" x = x
thus  x "\/" x = x ; ::_thesis: verum
end;
 for b being Element of the 1 -element Lattice ex a being Element of the 1 -element Lattice st a is_a_complement'_of b
proof
let b be Element of the 1 -element Lattice; ::_thesis: ex a being Element of the 1 -element Lattice st a is_a_complement'_of b
take a = b; ::_thesis: a is_a_complement'_of b
 ( b "\/" a = Top' the 1 -element Lattice & b "/\" a = Bot' the 1 -element Lattice ) by STRUCT_0:def_10;
hence  a is_a_complement'_of b by Def6; ::_thesis: verum
end;
then A5: the 1 -element Lattice is complemented' by Def7;
 for a, b, c being Element of the 1 -element Lattice holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) by STRUCT_0:def_10;
then A6: the 1 -element Lattice is distributive by LATTICES:def_11;
A7: the 1 -element Lattice is lower-bounded'
proof
set x = the Element of the 1 -element Lattice;
 for y being Element of the 1 -element Lattice holds
( the Element of the 1 -element Lattice "\/" y = y & y "\/" the Element of the 1 -element Lattice = y ) by STRUCT_0:def_10;
hence  the 1 -element Lattice is lower-bounded' by Def3; ::_thesis: verum
end;
A8: the 1 -element Lattice is upper-bounded'
proof
set x = the Element of the 1 -element Lattice;
 for y being Element of the 1 -element Lattice holds
( the Element of the 1 -element Lattice "/\" y = y & y "/\" the Element of the 1 -element Lattice = y ) by STRUCT_0:def_10;
hence  the 1 -element Lattice is upper-bounded' by Def1; ::_thesis: verum
end;
 for a, b, c being Element of the 1 -element Lattice holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) by STRUCT_0:def_10;
then  the 1 -element Lattice is distributive' by Def5;
hence  ex b1 being 1 -element LattStr st
( b1 is Boolean & b1 is join-idempotent & b1 is upper-bounded' & b1 is complemented' & b1 is distributive' & b1 is lower-bounded' & b1 is Lattice-like ) by A3, A6, A1, A2, A4, A8, A5, A7; ::_thesis: verum
end;
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
proof
let L be non empty join-commutative meet-commutative distributive upper-bounded' distributive' complemented' LattStr ; ::_thesis: for x being Element of L holds x "\/" (x `#) = Top' L
let x be Element of L; ::_thesis: x "\/" (x `#) = Top' L
 x `# is_a_complement'_of x by Def8;
hence  x "\/" (x `#) = Top' L by Def6; ::_thesis: verum
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
proof
let L be non empty join-commutative meet-commutative distributive upper-bounded' distributive' complemented' LattStr ; ::_thesis: for x being Element of L holds x "/\" (x `#) = Bot' L
let x be Element of L; ::_thesis: x "/\" (x `#) = Bot' L
 x `# is_a_complement'_of x by Def8;
hence  x "/\" (x `#) = Bot' L by Def6; ::_thesis: verum
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
proof
let L be non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' distributive' complemented' LattStr ; ::_thesis: for x being Element of L holds x "\/" (Top' L) = Top' L
let x be Element of L; ::_thesis: x "\/" (Top' L) = Top' 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  x "\/" (Top' L) = Top' L ; ::_thesis: verum
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
proof
let L be non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr ; ::_thesis: for x being Element of L holds x "/\" (Bot' L) = Bot' L
let x be Element of L; ::_thesis: x "/\" (Bot' L) = Bot' 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  x "/\" (Bot' L) = Bot' L ; ::_thesis: verum
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
proof
let L be non empty join-commutative meet-commutative meet-absorbing join-absorbing distributive join-idempotent LattStr ; ::_thesis: for x, y, z being Element of L holds ((x "\/" y) "\/" z) "/\" x = x
let x, y, z be Element of L; ::_thesis: ((x "\/" y) "\/" z) "/\" x = x
((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  ((x "\/" y) "\/" z) "/\" x = x ; ::_thesis: verum
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
proof
let L be non empty join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent distributive' LattStr ; ::_thesis: for x, y, z being Element of L holds ((x "/\" y) "/\" z) "\/" x = x
let x, y, z be Element of L; ::_thesis: ((x "/\" y) "/\" z) "\/" x = x
((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  ((x "/\" y) "/\" z) "\/" x = x ; ::_thesis: verum
end;

definition
let G be non empty /\-SemiLattStr ;
attrG is meet-idempotent  means :Def9: :: SHEFFER1:def 9
 for x being Element of G holds x "/\" x = x;
end;

:: deftheorem Def9 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 );

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
let L be non empty join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' complemented' LattStr ; ::_thesis: L is meet-idempotent
now__::_thesis:_for_x_being_Element_of_L_holds_x_"/\"_x_=_x
let x be Element of L; ::_thesis: x "/\" x = x
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 ; ::_thesis: verum
end;
hence  L is meet-idempotent by Def9; ::_thesis: verum
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
let L be non empty join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' complemented' LattStr ; ::_thesis: L is join-idempotent
let x be Element of L; :: according to ROBBINS1:def_7 ::_thesis: x "\/" x = x
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 ; ::_thesis: verum
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
let L be non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' distributive' complemented' LattStr ; ::_thesis: L is meet-absorbing
let y, x be Element of L; :: according to LATTICES:def_8 ::_thesis: (y "/\" x) "\/" x = x
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  (y "/\" x) "\/" x = x ; ::_thesis: verum
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
let L be non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr ; ::_thesis: L is join-absorbing
let x, y be Element of L; :: according to LATTICES:def_9 ::_thesis: x "/\" (x "\/" y) = x
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, Def9
.= x by A2, LATTICES:def_8 ;
hence  x "/\" (x "\/" y) = x ; ::_thesis: verum
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
let L be non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr ; ::_thesis: L is upper-bounded
 ex c being Element of L st
for a being Element of L holds
( c "\/" a = c & a "\/" c = c )
proof
take  Top' L ; ::_thesis: for a being Element of L holds
( (Top' L) "\/" a = Top' L & a "\/" (Top' L) = Top' L )
let a be Element of L; ::_thesis: ( (Top' L) "\/" a = Top' L & a "\/" (Top' L) = Top' L )
thus  ( (Top' L) "\/" a = Top' L & a "\/" (Top' L) = Top' L ) by Th4; ::_thesis: verum
end;
hence  L is upper-bounded by LATTICES:def_14; ::_thesis: verum
end;

theorem Th13: :: SHEFFER1:13
for L being non empty Lattice-like Boolean LattStr holds L is upper-bounded'
proof
let L be non empty Lattice-like Boolean LattStr ; ::_thesis: L is upper-bounded'
 ex c being Element of L st
for a being Element of L holds
( c "/\" a = a & a "/\" c = a )
proof
take c = Top L; ::_thesis: for a being Element of L holds
( c "/\" a = a & a "/\" c = a )
let a be Element of L; ::_thesis: ( c "/\" a = a & a "/\" c = a )
 a [= c by LATTICES:19;
hence  ( c "/\" a = a & a "/\" c = a ) by LATTICES:4; ::_thesis: verum
end;
hence  L is upper-bounded' by Def1; ::_thesis: verum
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
let L be non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr ; ::_thesis: L is lower-bounded
 ex c being Element of L st
for a being Element of L holds
( c "/\" a = c & a "/\" c = c )
proof
take  Bot' L ; ::_thesis: for a being Element of L holds
( (Bot' L) "/\" a = Bot' L & a "/\" (Bot' L) = Bot' L )
let a be Element of L; ::_thesis: ( (Bot' L) "/\" a = Bot' L & a "/\" (Bot' L) = Bot' L )
thus  ( (Bot' L) "/\" a = Bot' L & a "/\" (Bot' L) = Bot' L ) by Th5; ::_thesis: verum
end;
hence  L is lower-bounded by LATTICES:def_13; ::_thesis: verum
end;

theorem Th15: :: SHEFFER1:15
for L being non empty Lattice-like Boolean LattStr holds L is lower-bounded'
proof
let L be non empty Lattice-like Boolean LattStr ; ::_thesis: L is lower-bounded'
 ex c being Element of L st
for a being Element of L holds
( c "\/" a = a & a "\/" c = a )
proof
take c = Bottom L; ::_thesis: for a being Element of L holds
( c "\/" a = a & a "\/" c = a )
let a be Element of L; ::_thesis: ( c "\/" a = a & a "\/" c = a )
 c [= a by LATTICES:16;
hence  ( c "\/" a = a & a "\/" c = a ) by LATTICES:def_3; ::_thesis: verum
end;
hence  L is lower-bounded' by Def3; ::_thesis: verum
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
let L be non empty join-commutative meet-commutative meet-absorbing join-absorbing distributive join-idempotent LattStr ; ::_thesis: L is join-associative
let x, y, z be Element of L; :: according to LATTICES:def_5 ::_thesis: x "\/" (y "\/" z) = (x "\/" y) "\/" z
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: ((x "\/" y) "\/" z) "/\" (x "\/" (y "\/" z)) = ((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 ;
((x "\/" y) "\/" z) "/\" (x "\/" (y "\/" z)) = (((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  x "\/" (y "\/" z) = (x "\/" y) "\/" z by A3; ::_thesis: verum
end;
hence  x "\/" (y "\/" z) = (x "\/" y) "\/" z ; ::_thesis: verum
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
let L be non empty join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent distributive' LattStr ; ::_thesis: L is meet-associative
let x, y, z be Element of L; :: according to LATTICES:def_7 ::_thesis: x "/\" (y "/\" z) = (x "/\" y) "/\" z
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: ((x "/\" y) "/\" z) "\/" (x "/\" (y "/\" z)) = ((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 ;
((x "/\" y) "/\" z) "\/" (x "/\" (y "/\" z)) = (((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  x "/\" (y "/\" z) = (x "/\" y) "/\" z by A3; ::_thesis: verum
end;
hence  x "/\" (y "/\" z) = (x "/\" y) "/\" z ; ::_thesis: verum
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
let L be non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr ; ::_thesis: Top L = Top' L
set Y = Top' L;
 ( L is upper-bounded & ( for a being Element of L holds
( (Top' L) "\/" a = Top' L & a "\/" (Top' L) = Top' L ) ) ) by Th4, Th12;
hence  Top L = Top' L by LATTICES:def_17; ::_thesis: verum
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
let L be non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr ; ::_thesis: Bottom L = Bot' L
set Y = Bot' L;
 ( L is lower-bounded & ( for a being Element of L holds
( (Bot' L) "/\" a = Bot' L & a "/\" (Bot' L) = Bot' L ) ) ) by Th5, Th14;
hence  Bottom L = Bot' L by LATTICES:def_16; ::_thesis: verum
end;

theorem Th20: :: SHEFFER1:20
for L being non empty Lattice-like Boolean distributive' LattStr holds Top L = Top' L
proof
let L be non empty Lattice-like Boolean distributive' LattStr ; ::_thesis: Top L = Top' L
set Y = Top L;
 ( L is upper-bounded' & ( for a being Element of L holds
( (Top L) "/\" a = a & a "/\" (Top L) = a ) ) ) by Th13;
hence  Top L = Top' L by Def2; ::_thesis: verum
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
let L be non empty Lattice-like distributive lower-bounded upper-bounded complemented Boolean distributive' LattStr ; ::_thesis: Bottom L = Bot' L
set Y = Bottom L;
 ( L is lower-bounded' & ( for a being Element of L holds
( (Bottom L) "\/" a = a & a "\/" (Bottom L) = a ) ) ) by Th15;
hence  Bottom L = Bot' L by Def4; ::_thesis: verum
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 )
proof
let L be non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr ; ::_thesis: for x, y being Element of L holds
( x is_a_complement'_of y iff x is_a_complement_of y )
let x, y be Element of L; ::_thesis: ( x is_a_complement'_of y iff x is_a_complement_of y )
hereby  ::_thesis: ( x is_a_complement_of y implies x is_a_complement'_of y )
assume A1: x is_a_complement'_of y ; ::_thesis: x is_a_complement_of y
then  x "/\" y = Bot' L by Def6;
then A2: x "/\" y = Bottom L by Th19;
 x "\/" y = Top' L by A1, Def6;
then  x "\/" y = Top L by Th18;
hence  x is_a_complement_of y by A2, LATTICES:def_18; ::_thesis: verum
end;
assume A3: x is_a_complement_of y ; ::_thesis: x is_a_complement'_of y
then  x "/\" y = Bottom L by LATTICES:def_18;
then A4: x "/\" y = Bot' L by Th19;
 x "\/" y = Top L by A3, LATTICES:def_18;
then  x "\/" y = Top' L by Th18;
hence  x is_a_complement'_of y by A4, Def6; ::_thesis: verum
end;

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
let L be non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr ; ::_thesis: L is complemented
 for b being Element of L ex a being Element of L st a is_a_complement_of b
proof
let b be Element of L; ::_thesis: ex a being Element of L st a is_a_complement_of b
consider a being Element of L such that
A1: a is_a_complement'_of b by Def7;
 b "/\" a = Bot' L by A1, Def6;
then A2: b "/\" a = Bottom L by Th19;
 b "\/" a = Top' L by A1, Def6;
then  b "\/" a = Top L by Th18;
then  a is_a_complement_of b by A2, LATTICES:def_18;
hence  ex a being Element of L st a is_a_complement_of b ; ::_thesis: verum
end;
hence  L is complemented by LATTICES:def_19; ::_thesis: verum
end;

theorem Th24: :: SHEFFER1:24
for L being non empty Lattice-like Boolean upper-bounded' lower-bounded' distributive' LattStr holds L is complemented'
proof
let L be non empty Lattice-like Boolean upper-bounded' lower-bounded' distributive' LattStr ; ::_thesis: L is complemented'
 for b being Element of L ex a being Element of L st a is_a_complement'_of b
proof
let b be Element of L; ::_thesis: ex a being Element of L st a is_a_complement'_of b
consider a being Element of L such that
A1: a is_a_complement_of b by LATTICES:def_19;
 b "/\" a = Bottom L by A1, LATTICES:def_18;
then A2: b "/\" a = Bot' L by Th21;
 b "\/" a = Top L by A1, LATTICES:def_18;
then  b "\/" a = Top' L by Th20;
then  a is_a_complement'_of b by A2, Def6;
hence  ex a being Element of L st a is_a_complement'_of b ; ::_thesis: verum
end;
hence  L is complemented' by Def7; ::_thesis: verum
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' ) )
proof
let L be non empty LattStr ; ::_thesis: ( 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' ) )
thus  ( L is Boolean Lattice implies ( 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' ) ) ::_thesis: ( 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' implies L is Boolean Lattice )
proof
assume A1: L is Boolean Lattice ; ::_thesis: ( 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' )
then reconsider L9 = L as Boolean Lattice ;
 ex c being Element of L9 st
for a being Element of L9 holds
( c "\/" a = a & a "\/" c = a )
proof
take  Bottom L9 ; ::_thesis: for a being Element of L9 holds
( (Bottom L9) "\/" a = a & a "\/" (Bottom L9) = a )
thus  for a being Element of L9 holds
( (Bottom L9) "\/" a = a & a "\/" (Bottom L9) = a ) ; ::_thesis: verum
end;
hence A2: L is lower-bounded' by Def3; ::_thesis: ( L is upper-bounded' & L is join-commutative & L is meet-commutative & L is distributive & L is distributive' & L is complemented' )
 ex c being Element of L9 st
for a being Element of L9 holds
( c "/\" a = a & a "/\" c = a )
proof
take  Top L9 ; ::_thesis: for a being Element of L9 holds
( (Top L9) "/\" a = a & a "/\" (Top L9) = a )
thus  for a being Element of L9 holds
( (Top L9) "/\" a = a & a "/\" (Top L9) = a ) ; ::_thesis: verum
end;
hence A3: L is upper-bounded' by Def1; ::_thesis: ( L is join-commutative & L is meet-commutative & L is distributive & L is distributive' & L is complemented' )
thus  ( L is join-commutative & L is meet-commutative ) by A1; ::_thesis: ( L is distributive & L is distributive' & L is complemented' )
 for a, b, c being Element of L9 holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) by LATTICES:def_11;
then  for a, b, c being Element of L9 holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) by LATTICES:3;
hence  ( L is distributive & L is distributive' ) by Def5; ::_thesis: L is complemented'
hence  L is complemented' by A1, A2, A3, Th24; ::_thesis: verum
end;
thus  ( 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' implies L is Boolean Lattice ) ::_thesis: verum
proof
assume  ( 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' ) ; ::_thesis: L is Boolean Lattice
then reconsider L9 = L as non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' 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 & L9 is join-absorbing ) by Th10, Th11;
then  ( L9 is join-associative & L9 is meet-associative ) by Th16, Th17;
hence  L is Boolean Lattice by A5, A4, A6; ::_thesis: verum
end;
end;

registration
cluster non empty Lattice-like Boolean  ->  non empty join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' complemented' for LattStr ;
coherence
 for b1 being non empty LattStr st b1 is Boolean & b1 is Lattice-like holds
( b1 is lower-bounded' & b1 is upper-bounded' & b1 is complemented' & b1 is join-commutative & b1 is meet-commutative & b1 is distributive & b1 is distributive' ) by Th25;
cluster non empty join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' complemented'  ->  non empty Lattice-like Boolean for LattStr ;
coherence
 for b1 being non empty LattStr st b1 is lower-bounded' & b1 is upper-bounded' & b1 is complemented' & b1 is join-commutative & b1 is meet-commutative & b1 is distributive & b1 is distributive' holds
( b1 is Boolean & b1 is Lattice-like ) by Th25;
end;

begin

definition
attrc1 is strict ;
struct ShefferStr  ->  1-sorted ;
aggrShefferStr(# carrier, stroke #) ->  ShefferStr ;
sel stroke c1 ->  BinOp of the carrier of c1;
end;

definition
attrc1 is strict ;
struct ShefferLattStr  ->  ShefferStr , LattStr ;
aggrShefferLattStr(# carrier, L_join, L_meet, stroke #) ->  ShefferLattStr ;
end;

definition
attrc1 is strict ;
struct ShefferOrthoLattStr  ->  ShefferStr , OrthoLattStr ;
aggrShefferOrthoLattStr(# carrier, L_join, L_meet, Compl, stroke #) ->  ShefferOrthoLattStr ;
end;

definition
func TrivShefferOrthoLattStr  ->  ShefferOrthoLattStr  equals :: SHEFFER1:def 10
 ShefferOrthoLattStr(# 1,op2,op2,op1,op2 #);
coherence
 ShefferOrthoLattStr(# 1,op2,op2,op1,op2 #) is ShefferOrthoLattStr ;
end;

:: deftheorem  defines TrivShefferOrthoLattStr SHEFFER1:def_10_:_
 TrivShefferOrthoLattStr = ShefferOrthoLattStr(# 1,op2,op2,op1,op2 #);

registration
cluster1 -element for ShefferStr ;
existence
 ex b1 being ShefferStr st b1 is 1 -element
proof
set S = {{}};
set B = the BinOp of {{}};
take  ShefferStr(# {{}}, the BinOp of {{}} #) ; ::_thesis: ShefferStr(# {{}}, the BinOp of {{}} #) is 1 -element
thus  the carrier of ShefferStr(# {{}}, the BinOp of {{}} #) is 1 -element ; :: according to STRUCT_0:def_19 ::_thesis: verum
end;
cluster1 -element for ShefferLattStr ;
existence
 ex b1 being ShefferLattStr st b1 is 1 -element
proof
set S = {{}};
set B = the BinOp of {{}};
take  ShefferLattStr(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}} #) ; ::_thesis: ShefferLattStr(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}} #) is 1 -element
thus  the carrier of ShefferLattStr(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}} #) is 1 -element ; :: according to STRUCT_0:def_19 ::_thesis: verum
end;
cluster1 -element for ShefferOrthoLattStr ;
existence
 ex b1 being ShefferOrthoLattStr st b1 is 1 -element
proof
set S = {{}};
set B = the BinOp of {{}};
set A = the UnOp of {{}};
take  ShefferOrthoLattStr(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the UnOp of {{}}, the BinOp of {{}} #) ; ::_thesis: ShefferOrthoLattStr(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the UnOp of {{}}, the BinOp of {{}} #) is 1 -element
thus  the carrier of ShefferOrthoLattStr(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the UnOp of {{}}, the BinOp of {{}} #) is 1 -element ; :: according to STRUCT_0:def_19 ::_thesis: verum
end;
end;

definition
let L be non empty ShefferStr ;
let x, y be Element of L;
funcx | y ->  Element of L equals :: SHEFFER1:def 11
 the stroke of L . (x,y);
coherence
 the stroke of L . (x,y) is Element of L ;
end;

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

definition
let L be non empty ShefferOrthoLattStr ;
attrL 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 `) ) );
end;

:: 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 `) ) ) );

definition
let L be non empty ShefferStr ;
attrL is satisfying_Sheffer_1  means :Def13: :: SHEFFER1:def 13
 for x being Element of L holds (x | x) | (x | x) = x;
attrL is satisfying_Sheffer_2  means :Def14: :: SHEFFER1:def 14
 for x, y being Element of L holds x | (y | (y | y)) = x | x;
attrL is satisfying_Sheffer_3  means :Def15: :: SHEFFER1:def 15
 for x, y, z being Element of L holds (x | (y | z)) | (x | (y | z)) = ((y | y) | x) | ((z | z) | x);
end;

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

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

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

registration
cluster1 -element  -> 1 -element satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 for ShefferStr ;
coherence
 for b1 being 1 -element ShefferStr holds
( b1 is satisfying_Sheffer_1 & b1 is satisfying_Sheffer_2 & b1 is satisfying_Sheffer_3 )
proof
let L be 1 -element ShefferStr ; ::_thesis: ( L is satisfying_Sheffer_1 & L is satisfying_Sheffer_2 & L is satisfying_Sheffer_3 )
thus  L is satisfying_Sheffer_1 ::_thesis: ( L is satisfying_Sheffer_2 & L is satisfying_Sheffer_3 )
proof
let x be Element of L; :: according to SHEFFER1:def_13 ::_thesis: (x | x) | (x | x) = x
thus  (x | x) | (x | x) = x by STRUCT_0:def_10; ::_thesis: verum
end;
thus  L is satisfying_Sheffer_2 ::_thesis: L is satisfying_Sheffer_3
proof
let x, y be Element of L; :: according to SHEFFER1:def_14 ::_thesis: x | (y | (y | y)) = x | x
thus  x | (y | (y | y)) = x | x by STRUCT_0:def_10; ::_thesis: verum
end;
let x, y, z be Element of L; :: according to SHEFFER1:def_15 ::_thesis: (x | (y | z)) | (x | (y | z)) = ((y | y) | x) | ((z | z) | x)
thus  (x | (y | z)) | (x | (y | z)) = ((y | y) | x) | ((z | z) | x) by STRUCT_0:def_10; ::_thesis: verum
end;
end;

registration
cluster1 -element  -> 1 -element join-commutative join-associative for \/-SemiLattStr ;
coherence
 for b1 being 1 -element \/-SemiLattStr holds
( b1 is join-commutative & b1 is join-associative )
proof
let L be 1 -element \/-SemiLattStr ; ::_thesis: ( L is join-commutative & L is join-associative )
thus  L is join-commutative ::_thesis: L is join-associative
proof
let x, y be Element of L; :: according to LATTICES:def_4 ::_thesis: x "\/" y = y "\/" x
thus  x "\/" y = y "\/" x by STRUCT_0:def_10; ::_thesis: verum
end;
let x, y, z be Element of L; :: according to LATTICES:def_5 ::_thesis: x "\/" (y "\/" z) = (x "\/" y) "\/" z
thus  x "\/" (y "\/" z) = (x "\/" y) "\/" z by STRUCT_0:def_10; ::_thesis: verum
end;
cluster1 -element  -> 1 -element meet-commutative meet-associative for /\-SemiLattStr ;
coherence
 for b1 being 1 -element /\-SemiLattStr holds
( b1 is meet-commutative & b1 is meet-associative )
proof
let L be 1 -element /\-SemiLattStr ; ::_thesis: ( L is meet-commutative & L is meet-associative )
thus  L is meet-commutative ::_thesis: L is meet-associative
proof
let x, y be Element of L; :: according to LATTICES:def_6 ::_thesis: x "/\" y = y "/\" x
thus  x "/\" y = y "/\" x by STRUCT_0:def_10; ::_thesis: verum
end;
let x, y, z be Element of L; :: according to LATTICES:def_7 ::_thesis: x "/\" (y "/\" z) = (x "/\" y) "/\" z
thus  x "/\" (y "/\" z) = (x "/\" y) "/\" z by STRUCT_0:def_10; ::_thesis: verum
end;
end;

registration
cluster1 -element  -> 1 -element meet-absorbing join-absorbing Boolean for LattStr ;
coherence
 for b1 being 1 -element LattStr holds
( b1 is join-absorbing & b1 is meet-absorbing & b1 is Boolean )
proof
let L be 1 -element LattStr ; ::_thesis: ( L is join-absorbing & L is meet-absorbing & L is Boolean )
thus  L is join-absorbing ::_thesis: ( L is meet-absorbing & L is Boolean )
proof
let x, y be Element of L; :: according to LATTICES:def_9 ::_thesis: x "/\" (x "\/" y) = x
thus  x "/\" (x "\/" y) = x by STRUCT_0:def_10; ::_thesis: verum
end;
A1: L is upper-bounded
proof
set c = the Element of L;
take  the Element of L ; :: according to LATTICES:def_14 ::_thesis: for b1 being M2( the carrier of L) holds
( the Element of L "\/" b1 = the Element of L & b1 "\/" the Element of L = the Element of L )
let a be Element of L; ::_thesis: ( the Element of L "\/" a = the Element of L & a "\/" the Element of L = the Element of L )
thus  ( the Element of L "\/" a = the Element of L & a "\/" the Element of L = the Element of L ) by STRUCT_0:def_10; ::_thesis: verum
end;
thus  L is meet-absorbing ::_thesis: L is Boolean
proof
let x, y be Element of L; :: according to LATTICES:def_8 ::_thesis: (x "/\" y) "\/" y = y
thus  (x "/\" y) "\/" y = y by STRUCT_0:def_10; ::_thesis: verum
end;
A2: L is lower-bounded
proof
set c = the Element of L;
take  the Element of L ; :: according to LATTICES:def_13 ::_thesis: for b1 being M2( the carrier of L) holds
( the Element of L "/\" b1 = the Element of L & b1 "/\" the Element of L = the Element of L )
let a be Element of L; ::_thesis: ( the Element of L "/\" a = the Element of L & a "/\" the Element of L = the Element of L )
thus  ( the Element of L "/\" a = the Element of L & a "/\" the Element of L = the Element of L ) by STRUCT_0:def_10; ::_thesis: verum
end;
A3: L is complemented
proof
set a = the Element of L;
let b be Element of L; :: according to LATTICES:def_19 ::_thesis: ex b1 being M2( the carrier of L) st b1 is_a_complement_of b
take  the Element of L ; ::_thesis: the Element of L is_a_complement_of b
A4: ( the Element of L "/\" b = Bottom L & b "/\" the Element of L = Bottom L ) by STRUCT_0:def_10;
 ( the Element of L "\/" b = Top L & b "\/" the Element of L = Top L ) by STRUCT_0:def_10;
hence  the Element of L is_a_complement_of b by A4, LATTICES:def_18; ::_thesis: verum
end;
 L is distributive
proof
let a, b, c be Element of L; :: according to LATTICES:def_11 ::_thesis: a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
thus  a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) by STRUCT_0:def_10; ::_thesis: verum
end;
hence  L is Boolean by A2, A1, A3; ::_thesis: verum
end;
end;

registration
cluster TrivShefferOrthoLattStr  -> 1 -element ;
coherence
 TrivShefferOrthoLattStr is 1 -element by CARD_1:49, STRUCT_0:def_19;
cluster TrivShefferOrthoLattStr  ->  well-complemented properly_defined ;
coherence
 ( TrivShefferOrthoLattStr is properly_defined & TrivShefferOrthoLattStr is well-complemented )
proof
set L = TrivShefferOrthoLattStr ;
A1: ( ( for x, y being Element of TrivShefferOrthoLattStr holds x "/\" y = (x | y) | (x | y) ) & ( for x, y being Element of TrivShefferOrthoLattStr holds x | y = (x `) + (y `) ) ) by STRUCT_0:def_10;
 ( ( for x being Element of TrivShefferOrthoLattStr holds x | x = x ` ) & ( for x, y being Element of TrivShefferOrthoLattStr holds x "\/" y = (x | x) | (y | y) ) ) by STRUCT_0:def_10;
hence  TrivShefferOrthoLattStr is properly_defined by A1, Def12; ::_thesis: TrivShefferOrthoLattStr is well-complemented
 TrivShefferOrthoLattStr is well-complemented
proof
let a be Element of TrivShefferOrthoLattStr; :: according to ROBBINS1:def_10 ::_thesis: a ` is_a_complement_of a
 ( a "\/" (a `) = Top TrivShefferOrthoLattStr & a "/\" (a `) = Bottom TrivShefferOrthoLattStr ) by STRUCT_0:def_10;
hence  a ` is_a_complement_of a by LATTICES:def_18; ::_thesis: verum
end;
hence  TrivShefferOrthoLattStr is well-complemented ; ::_thesis: verum
end;
end;

registration
cluster non empty Lattice-like Boolean well-complemented properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 for ShefferOrthoLattStr ;
existence
 ex b1 being non empty ShefferOrthoLattStr st
( b1 is properly_defined & b1 is Boolean & b1 is well-complemented & b1 is Lattice-like & b1 is satisfying_Sheffer_1 & b1 is satisfying_Sheffer_2 & b1 is satisfying_Sheffer_3 )
proof
take  TrivShefferOrthoLattStr ; ::_thesis: ( TrivShefferOrthoLattStr is properly_defined & TrivShefferOrthoLattStr is Boolean & TrivShefferOrthoLattStr is well-complemented & TrivShefferOrthoLattStr is Lattice-like & TrivShefferOrthoLattStr is satisfying_Sheffer_1 & TrivShefferOrthoLattStr is satisfying_Sheffer_2 & TrivShefferOrthoLattStr is satisfying_Sheffer_3 )
thus  ( TrivShefferOrthoLattStr is properly_defined & TrivShefferOrthoLattStr is Boolean & TrivShefferOrthoLattStr is well-complemented & TrivShefferOrthoLattStr is Lattice-like & TrivShefferOrthoLattStr is satisfying_Sheffer_1 & TrivShefferOrthoLattStr is satisfying_Sheffer_2 & TrivShefferOrthoLattStr is satisfying_Sheffer_3 ) ; ::_thesis: verum
end;
end;

theorem :: SHEFFER1:26
for L being non empty Lattice-like Boolean well-complemented properly_defined ShefferOrthoLattStr holds L is satisfying_Sheffer_1
proof
let L be non empty Lattice-like Boolean well-complemented properly_defined ShefferOrthoLattStr ; ::_thesis: L is satisfying_Sheffer_1
let x be Element of L; :: according to SHEFFER1:def_13 ::_thesis: (x | x) | (x | x) = x
 (x `) ` = x by ROBBINS1:3;
then  (x | x) ` = x by Def12;
hence  (x | x) | (x | x) = x by Def12; ::_thesis: verum
end;

theorem :: SHEFFER1:27
for L being non empty Lattice-like Boolean well-complemented properly_defined ShefferOrthoLattStr holds L is satisfying_Sheffer_2
proof
let L be non empty Lattice-like Boolean well-complemented properly_defined ShefferOrthoLattStr ; ::_thesis: L is satisfying_Sheffer_2
let x, y be Element of L; :: according to SHEFFER1:def_14 ::_thesis: x | (y | (y | y)) = x | x
 (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  x | (y | (y | y)) = x | x ; ::_thesis: verum
end;

theorem :: SHEFFER1:28
for L being non empty Lattice-like Boolean well-complemented properly_defined ShefferOrthoLattStr holds L is satisfying_Sheffer_3
proof
let L be non empty Lattice-like Boolean well-complemented properly_defined ShefferOrthoLattStr ; ::_thesis: L is satisfying_Sheffer_3
let x, y, z be Element of L; :: according to SHEFFER1:def_15 ::_thesis: (x | (y | z)) | (x | (y | z)) = ((y | y) | x) | ((z | z) | x)
 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  (x | (y | z)) | (x | (y | z)) = ((y | y) | x) | ((z | z) | x) ; ::_thesis: verum
end;

definition
let L be non empty ShefferStr ;
let a be Element of L;
funca "  ->  Element of L equals :: SHEFFER1:def 16
a | a;
coherence
 a | a is Element of L ;
end;

:: deftheorem  defines " SHEFFER1:def_16_:_
 for L being non empty ShefferStr
for a being Element of L holds a " = a | a;

theorem :: SHEFFER1:29
for L being non empty satisfying_Sheffer_3 ShefferOrthoLattStr
for x, y, z being Element of L holds (x | (y | z)) " = ((y ") | x) | ((z ") | x) by Def15;

theorem :: SHEFFER1:30
for L being non empty satisfying_Sheffer_1 ShefferOrthoLattStr
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
proof
let L be non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr ; ::_thesis: for x, y being Element of L holds x | y = y | x
let x, y be Element of L; ::_thesis: x | y = y | x
x | y = ((x | y) ") " by Def13
.= ((x | ((y ") ")) ") " by Def13
.= ((((y ") ") | x) ") " by Def15
.= ((y | x) ") " by Def13
.= y | x by Def13 ;
hence  x | y = y | x ; ::_thesis: verum
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)
proof
let L be non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr ; ::_thesis: for x, y being Element of L holds x | (x | x) = y | (y | y)
let x, y be Element of L; ::_thesis: x | (x | x) = y | (y | y)
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  x | (x | x) = y | (y | y) ; ::_thesis: verum
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
let L be non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr ; ::_thesis: L is join-commutative
let x, y be Element of L; :: according to LATTICES:def_4 ::_thesis: x "\/" y = y "\/" x
x "\/" y = (x ") | (y | y) by Def12
.= (y | y) | (x | x) by Th31
.= y "\/" x by Def12 ;
hence  x "\/" y = y "\/" x ; ::_thesis: verum
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
let L be non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr ; ::_thesis: L is meet-commutative
let x, y be Element of L; :: according to LATTICES:def_6 ::_thesis: x "/\" y = y "/\" x
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  x "/\" y = y "/\" x ; ::_thesis: verum
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
let L be non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr ; ::_thesis: L is distributive
let x, y, z be Element of L; :: according to LATTICES:def_11 ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
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  x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) ; ::_thesis: verum
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
let L be non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr ; ::_thesis: L is distributive'
let x, y, z be Element of L; :: according to SHEFFER1:def_5 ::_thesis: x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z)
set X = x | x;
x "\/" (y "/\" z) = x "\/" ((y | z) | (y | z)) by Def12
.= (x | x) | (((y | z) ") ") by Def12
.= (x | x) | (y | z) by Def13
.= (((x | x) | (y | z)) ") " by Def13
.= (((y ") | (x | x)) | ((z ") | (x | x))) " by Def15
.= (((x | x) | (y ")) | ((z ") | (x | x))) " by Th31
.= (((x | x) | (y | y)) | ((x | x) | (z "))) " by Th31
.= ((x "\/" y) | ((x | x) | (z | z))) | (((x | x) | (y | y)) | ((x | x) | (z | z))) by Def12
.= ((x "\/" y) | (x "\/" z)) | (((x | x) | (y | y)) | ((x | x) | (z | z))) by Def12
.= ((x "\/" y) | (x "\/" z)) | ((x "\/" y) | ((x | x) | (z | z))) by Def12
.= ((x "\/" y) | (x "\/" z)) | ((x "\/" y) | (x "\/" z)) by Def12
.= (x "\/" y) "/\" (x "\/" z) by Def12 ;
hence  x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z) ; ::_thesis: verum
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
let L be non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr ; ::_thesis: L is Boolean Lattice
A1: ( L is distributive & L is distributive' ) by Th35, Th36;
 ex c being Element of L st
for a being Element of L holds
( c "/\" a = a & a "/\" c = a )
proof
set b = the Element of L;
take c = ( the Element of L | the Element of L) | (( the Element of L | the Element of L) | ( the Element of L | the Element of L)); ::_thesis: for a being Element of L holds
( c "/\" a = a & a "/\" c = a )
let a be Element of L; ::_thesis: ( c "/\" a = a & a "/\" c = a )
thus  c "/\" a = a ::_thesis: a "/\" c = a
proof
set X = the Element of L " ;
c "/\" a = ((( the Element of L | the Element of L) | (( the Element of L ") | ( the Element of L "))) | a) " by Def12
.= (a | (( the Element of L ") | (( the Element of L ") | ( the Element of L ")))) " by Th31
.= (a | a) " by Def14
.= a by Def13 ;
hence  c "/\" a = a ; ::_thesis: verum
end;
thus  a "/\" c = a ::_thesis: verum
proof
set X = the Element of L " ;
a "/\" c = (a | (( the Element of L | the Element of L) | (( the Element of L ") | ( the Element of L ")))) " by Def12
.= (a | a) " by Def14
.= a by Def13 ;
hence  a "/\" c = a ; ::_thesis: verum
end;
end;
then A2: L is upper-bounded' by Def1;
 ex c being Element of L st
for a being Element of L holds
( c "\/" a = a & a "\/" c = a )
proof
set b = the Element of L;
take c = ( the Element of L | ( the Element of L | the Element of L)) | ( the Element of L | ( the Element of L | the Element of L)); ::_thesis: for a being Element of L holds
( c "\/" a = a & a "\/" c = a )
let a be Element of L; ::_thesis: ( c "\/" a = a & a "\/" c = a )
c "\/" a = ((( the Element of L | ( the Element of L | the Element of L)) ") ") | (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 ; ::_thesis: a "\/" c = a
a "\/" c = (a | a) | ((( the Element of L | ( the Element of L | the Element of L)) ") ") 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 ; ::_thesis: verum
end;
then A3: L is lower-bounded' by Def3;
 for b being Element of L ex a being Element of L st a is_a_complement'_of b
proof
let b be Element of L; ::_thesis: ex a being Element of L st a is_a_complement'_of b
set a = b | b;
take  b | b ; ::_thesis: b | b is_a_complement'_of b
A4: Top' L = (b | b) | ((b | b) | (b | b))
proof
set X = (b | b) | ((b | b) | (b | b));
 for a being Element of L holds
( ((b | b) | ((b | b) | (b | b))) "/\" a = a & a "/\" ((b | b) | ((b | b) | (b | b))) = a )
proof
let a be Element of L; ::_thesis: ( ((b | b) | ((b | b) | (b | b))) "/\" a = a & a "/\" ((b | b) | ((b | b) | (b | b))) = a )
set Y = b " ;
thus ((b | b) | ((b | b) | (b | b))) "/\" a = (((b | b) | ((b ") | (b "))) | a) " by Def12
.= (a | ((b ") | ((b ") | (b ")))) " by Th31
.= (a | a) " by Def14
.= a by Def13 ; ::_thesis: a "/\" ((b | b) | ((b | b) | (b | b))) = a
thus a "/\" ((b | b) | ((b | b) | (b | b))) = (a | ((b | b) | ((b ") | (b ")))) " by Def12
.= (a | a) " by Def14
.= a by Def13 ; ::_thesis: verum
end;
hence  Top' L = (b | b) | ((b | b) | (b | b)) by A2, Def2; ::_thesis: verum
end;
then A5: b "\/" (b | b) = Top' L by Def12;
A6: Bot' L = (b | (b | b)) | (b | (b | b))
proof
set X = (b | (b | b)) | (b | (b | b));
 for a being Element of L holds
( ((b | (b | b)) | (b | (b | b))) "\/" a = a & a "\/" ((b | (b | b)) | (b | (b | b))) = a )
proof
let a be Element of L; ::_thesis: ( ((b | (b | b)) | (b | (b | b))) "\/" a = a & a "\/" ((b | (b | b)) | (b | (b | b))) = a )
thus ((b | (b | b)) | (b | (b | b))) "\/" 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 ; ::_thesis: a "\/" ((b | (b | b)) | (b | (b | b))) = a
thus a "\/" ((b | (b | b)) | (b | (b | b))) = (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 ; ::_thesis: verum
end;
hence  Bot' L = (b | (b | b)) | (b | (b | b)) by A3, Def4; ::_thesis: verum
end;
then A7: b "/\" (b | b) = Bot' L by Def12;
A8: (b | b) "\/" b = ((b | b) | (b | b)) | (b | b) by Def12
.= Top' L by A4, Th31 ;
(b | b) "/\" b = ((b | b) | b) | ((b | b) | b) by Def12
.= (b | (b | b)) | ((b | b) | b) by Th31
.= Bot' L by A6, Th31 ;
hence  b | b is_a_complement'_of b by A8, A5, A7, Def6; ::_thesis: verum
end;
then A9: L is complemented' by Def7;
 ( L is join-commutative & L is meet-commutative ) by Th33, Th34;
hence  L is Boolean Lattice by A3, A2, A9, A1; ::_thesis: verum
end;