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 c = Bottom L9; :: thesis: for a being Element of L9 holds
( c "\/" a = a & a "\/" c = a )
thus for a being Element of L9 holds
( c "\/" a = a & a "\/" c = a ) by LATTICES:39; :: thesis: verum

end;

hence A2: L is lower-bounded' by Def3; :: 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 c = Top L9; :: thesis: for a being Element of L9 holds
( c "/\" a = a & a "/\" c = a )
thus for a being Element of L9 holds
( c "/\" a = a & a "/\" c = a ) by LATTICES:43; :: thesis: verum

end;

hence A3: L is upper-bounded' by Def1; :: 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:19;
hence ( L is distributive & L is distributive' ) by Def5; :: thesis: L is complemented'
hence L is complemented' by A1, A2, A3, Th25; :: 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

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 Th10;
A4: L9 is complemented by Th24;
A5: ( L9 is lower-bounded & L9 is upper-bounded ) by Th13, Th15;
A6: ( L9 is meet-absorbing & L9 is join-absorbing ) by Th11, Th12;
then ( L9 is join-associative & L9 is meet-associative ) by Th17, Th18;
hence L is Boolean Lattice by A5, A4, A6; :: thesis: verum

end;