let L be well-complemented preOrthoLattice; :: thesis: ( L is Boolean implies L is Huntington )
assume A1: L is Boolean ; :: thesis: L is Huntington
then A2: ( L is bounded & L is distributive & L is complemented ) ;
reconsider L' = L as Boolean preOrthoLattice by A1;
A3: for x being Element of L' holds (Top L') "/\" 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 A2, Th34
.= (x + (((x ` ) + y) ` )) "/\" (y + (((x ` ) + y) ` )) by A2, LATTICES:31
.= (x + (((x ` ) + ((y ` ) ` )) ` )) "/\" (y + (((x ` ) + y) ` )) by A2, Th33
.= (x + (x "/\" (y ` ))) "/\" (y + (((x ` ) + y) ` )) by A2, Th34
.= x "/\" (y + (((x ` ) + y) ` )) by LATTICES:def 8
.= x "/\" (y + (((x ` ) + ((y ` ) ` )) ` )) by A2, Th33
.= x "/\" (y + (x "/\" (y ` ))) by A2, Th34
.= x "/\" ((y + x) "/\" (y + (y ` ))) by A2, 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 A3 ; :: thesis: verum

end;

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