let L be non empty LattStr ; :: thesis: ( L is Boolean Lattice iff ( L is lower-bounded' & L is upper-bounded' & L is join-commutative & L is meet-commutative & L is distributive & L is distributive' & L is complemented' ) )

thus ( L is Boolean Lattice implies ( L is lower-bounded' & L is upper-bounded' & L is join-commutative & L is meet-commutative & L is distributive & L is distributive' & L is complemented' ) ) :: thesis: ( L is lower-bounded' & L is upper-bounded' & L is join-commutative & L is meet-commutative & L is distributive & L is distributive' & L is complemented' implies L is Boolean Lattice )

thus ( L is Boolean Lattice implies ( L is lower-bounded' & L is upper-bounded' & L is join-commutative & L is meet-commutative & L is distributive & L is distributive' & L is complemented' ) ) :: thesis: ( L is lower-bounded' & L is upper-bounded' & L is join-commutative & L is meet-commutative & L is distributive & L is distributive' & L is complemented' implies L is Boolean Lattice )

proof

thus
( L is lower-bounded' & L is upper-bounded' & L is join-commutative & L is meet-commutative & L is distributive & L is distributive' & L is complemented' implies L is Boolean Lattice )
:: thesis: verum
assume A1:
L is Boolean Lattice
; :: thesis: ( L is lower-bounded' & L is upper-bounded' & L is join-commutative & L is meet-commutative & L is distributive & L is distributive' & L is complemented' )

then reconsider L9 = L as Boolean Lattice ;

ex c being Element of L9 st

for a being Element of L9 holds

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

ex c being Element of L9 st

for a being Element of L9 holds

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

thus ( L is join-commutative & L is meet-commutative ) by A1; :: thesis: ( L is distributive & L is distributive' & L is complemented' )

for a, b, c being Element of L9 holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) by LATTICES:def 11;

then for a, b, c being Element of L9 holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) by LATTICES:3;

hence ( L is distributive & L is distributive' ) ; :: thesis: L is complemented'

hence L is complemented' by A1, A2, A3, Th24; :: thesis: verum

end;then reconsider L9 = L as Boolean Lattice ;

ex c being Element of L9 st

for a being Element of L9 holds

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

proof

hence A2:
L is lower-bounded'
; :: thesis: ( L is upper-bounded' & L is join-commutative & L is meet-commutative & L is distributive & L is distributive' & L is complemented' )
take
Bottom L9
; :: thesis: for a being Element of L9 holds

( (Bottom L9) "\/" a = a & a "\/" (Bottom L9) = a )

thus for a being Element of L9 holds

( (Bottom L9) "\/" a = a & a "\/" (Bottom L9) = a ) ; :: thesis: verum

end;( (Bottom L9) "\/" a = a & a "\/" (Bottom L9) = a )

thus for a being Element of L9 holds

( (Bottom L9) "\/" a = a & a "\/" (Bottom L9) = a ) ; :: thesis: verum

ex c being Element of L9 st

for a being Element of L9 holds

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

proof

hence A3:
L is upper-bounded'
; :: thesis: ( L is join-commutative & L is meet-commutative & L is distributive & L is distributive' & L is complemented' )
take
Top L9
; :: thesis: for a being Element of L9 holds

( (Top L9) "/\" a = a & a "/\" (Top L9) = a )

thus for a being Element of L9 holds

( (Top L9) "/\" a = a & a "/\" (Top L9) = a ) ; :: thesis: verum

end;( (Top L9) "/\" a = a & a "/\" (Top L9) = a )

thus for a being Element of L9 holds

( (Top L9) "/\" a = a & a "/\" (Top L9) = a ) ; :: thesis: verum

thus ( L is join-commutative & L is meet-commutative ) by A1; :: thesis: ( L is distributive & L is distributive' & L is complemented' )

for a, b, c being Element of L9 holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) by LATTICES:def 11;

then for a, b, c being Element of L9 holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) by LATTICES:3;

hence ( L is distributive & L is distributive' ) ; :: thesis: L is complemented'

hence L is complemented' by A1, A2, A3, Th24; :: thesis: verum

proof

assume
( L is lower-bounded' & L is upper-bounded' & L is join-commutative & L is meet-commutative & L is distributive & L is distributive' & L is complemented' )
; :: thesis: L is Boolean Lattice

then reconsider L9 = L as non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr by Th9;

A4: L9 is complemented by Th23;

A5: ( L9 is lower-bounded & L9 is upper-bounded ) by Th12, Th14;

A6: ( L9 is meet-absorbing & L9 is join-absorbing ) by Th10, Th11;

then ( L9 is join-associative & L9 is meet-associative ) by Th16, Th17;

hence L is Boolean Lattice by A5, A4, A6; :: thesis: verum

end;then reconsider L9 = L as non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr by Th9;

A4: L9 is complemented by Th23;

A5: ( L9 is lower-bounded & L9 is upper-bounded ) by Th12, Th14;

A6: ( L9 is meet-absorbing & L9 is join-absorbing ) by Th10, Th11;

then ( L9 is join-associative & L9 is meet-associative ) by Th16, Th17;

hence L is Boolean Lattice by A5, A4, A6; :: thesis: verum