let L be well-complemented preOrthoLattice; :: thesis: ( L is Boolean implies L is Huntington )
assume A1: L is Boolean ; :: thesis: L is Huntington
then reconsider L9 = L as Boolean preOrthoLattice ;
A2: for x being Element of L9 holds (Top L9) "/\" x = x by LATTICES:43;

now

let x, y be Element of L; :: thesis: (((x `) "\/" (y `)) `) "\/" (((x `) "\/" y) `) = x
thus (((x `) "\/" (y `)) `) "\/" (((x `) "\/" y) `) = (x "/\" y) + (((x `) + y) `) by A1, Th34
.= (x + (((x `) + y) `)) "/\" (y + (((x `) + y) `)) by A1, LATTICES:31
.= (x + (((x `) + ((y `) `)) `)) "/\" (y + (((x `) + y) `)) by A1, Th33
.= (x + (x "/\" (y `))) "/\" (y + (((x `) + y) `)) by A1, Th34
.= x "/\" (y + (((x `) + y) `)) by LATTICES:def 8
.= x "/\" (y + (((x `) + ((y `) `)) `)) by A1, Th33
.= x "/\" (y + (x "/\" (y `))) by A1, Th34
.= x "/\" ((y + x) "/\" (y + (y `))) by A1, LATTICES:31
.= (x "/\" (y + x)) "/\" (y + (y `)) by LATTICES:def 7
.= x "/\" (y + (y `)) by LATTICES:def 9
.= x "/\" (Top L) by Th61
.= x by A2 ; :: thesis: verum

end;

hence L is Huntington by Def6; :: thesis: verum