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 )

ex c being Element of L st

for a being Element of L holds

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

for b being Element of L ex a being Element of L st a is_a_complement'_of b

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

hence L is Boolean Lattice by A3, A2, A9, A1; :: thesis: verum

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

then A2:
L is upper-bounded'
;
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

end;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

thus
a "/\" c = a
:: thesis: verum
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;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

ex c being Element of L st

for a being Element of L holds

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

proof

then A3:
L is lower-bounded'
;
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;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

for b being Element of L ex a being Element of L st a is_a_complement'_of b

proof

then A9:
L is complemented'
;
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))

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

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

then A5:
b "\/" (b | b) = Top' L
by Def12;
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 )

end;for a being Element of L holds

( ((b | b) | ((b | b) | (b | b))) "/\" a = a & a "/\" ((b | b) | ((b | b) | (b | b))) = a )

proof

hence
Top' L = (b | b) | ((b | b) | (b | b))
by A2, Def2; :: thesis: verum
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;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

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

proof

then A7:
b "/\" (b | b) = Bot' L
by Def12;
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 )

end;for a being Element of L holds

( ((b | (b | b)) | (b | (b | b))) "\/" a = a & a "\/" ((b | (b | b)) | (b | (b | b))) = a )

proof

hence
Bot' L = (b | (b | b)) | (b | (b | b))
by A3, Def4; :: thesis: verum
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;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

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

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

hence L is Boolean Lattice by A3, A2, A9, A1; :: thesis: verum