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 L9 = L as Huntington preOrthoLattice ;
A2: L is lower-bounded
proof
set c9 = Bot L9;
reconsider c = Bot L9 as Element of L ;
take c ; :: according to LATTICES:def 13 :: thesis: for b1 being M3( the carrier of L) holds
( c "/\" b1 = c & b1 "/\" c = c )
let a be Element of L; :: thesis: ( c "/\" a = c & a "/\" c = c )
reconsider a9 = a as Element of L9 ;
thus c "/\" a = (Bot L9) *' a9 by Def23
.= c by Def9 ; :: thesis: a "/\" c = c
thus a "/\" c = (Bot L9) *' a9 by Def23
.= c by Def9 ; :: thesis: verum
end;
L9 is upper-bounded ;
hence L is bounded by A2; :: according to LATTICES:def 20 :: thesis: ( L is complemented & L is distributive )
thus L is complemented :: thesis: L is distributive
proof
let b be Element of L; :: according to LATTICES:def 19 :: thesis: ex b1 being M3( the carrier of L) st b1 is_a_complement_of b
take a = b ` ; :: thesis: a is_a_complement_of b
A3: L9 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 L9 by Th8
.= Bottom L by Th61 ; :: 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, Th30 ; :: thesis: verum
end;