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' ;
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' ;
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; :: thesis: verum

end;

then A9: L is complemented' ;
( L is join-commutative & L is meet-commutative ) by Th33, Th34;
hence L is Boolean Lattice by A3, A2, A9, A1; :: thesis: verum