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 )
proof
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 )
proof
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;
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' )
ex c being Element of L9 st
for a being Element of L9 holds
( c "/\" a = a & a "/\" c = a )
proof
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;
hence A3: L is upper-bounded' ; :: thesis: ( L is join-commutative & L is meet-commutative & L is distributive & L is distributive' & L is complemented' )
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:
hence L is complemented' by A1, A2, A3, Th24; :: thesis: verum
end;
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
proof end;