let L be de_Morgan preOrthoLattice; :: thesis: ( L is Huntington implies L is Boolean )
assume A1: L is Huntington ; :: thesis: L is Boolean
then reconsider L' = L as Huntington preOrthoLattice ;
thus L is bounded :: according to LATTICES:def 20 :: thesis: ( L is complemented & L is distributive )

proof

A2: L' is upper-bounded ;
L is lower-bounded

proof

set c' = Bot L';
reconsider c = Bot L' as Element of L ;
take c ; :: according to LATTICES:def 13 :: thesis: for b₁ being M2(the carrier of L) holds
( c "/\" b₁ = c & b₁ "/\" c = c )
let a be Element of L; :: thesis: ( c "/\" a = c & a "/\" c = c )
reconsider a' = a as Element of L' ;
thus c "/\" a = (Bot L') *' a' by Def23
.= c by Def9 ; :: thesis: a "/\" c = c
thus a "/\" c = (Bot L') *' a' by Def23
.= c by Def9 ; :: thesis: verum

end;

hence L is bounded by A2; :: thesis: verum

end;

thus L is complemented :: thesis: L is distributive

proof

let b be Element of L; :: according to LATTICES:def 19 :: thesis: ex b₁ being M2(the carrier of L) st b₁ is_a_complement_of b
take a = b ` ; :: thesis: a is_a_complement_of b
A3: L' is join-idempotent ;
hence a + b = Top L by Def8; :: according to LATTICES:def 18 :: thesis: ( b + a = Top L & a "/\" b = Bottom L & b "/\" a = Bottom L )
thus b + a = Top L by A3, Def8; :: thesis: ( a "/\" b = Bottom L & b "/\" a = Bottom L )
thus a "/\" b = ((a ` ) + (b ` )) ` by Def23
.= Bot L' by Th9
.= Bottom L by Th63 ; :: thesis: b "/\" a = Bottom L
hence b "/\" a = Bottom L ; :: thesis: verum

end;

thus L is distributive :: thesis: verum

proof

let a, b, c be Element of L; :: according to LATTICES:def 11 :: thesis: a "/\" (b + c) = (a "/\" b) + (a "/\" c)
A4: ( a "/\" b = a *' b & a "/\" c = a *' c ) by Def23;
thus a "/\" (b "\/" c) = a *' (b + c) by Def23
.= (a "/\" b) "\/" (a "/\" c) by A1, A4, Th31 ; :: thesis: verum

end;