Boolean algebras and their order

In ZF, a Boolean algebra is a set $B$ with binary operations $\wedge ,\vee$, a unary operation $\mathrm{\neg }$, and elements $0,1$, satisfying the bounded distributive lattice laws and

$a\wedge \mathrm{\neg }a=0,a\vee \mathrm{\neg }a=1(a\in B)\mathrm{.}$

Explicitly, both binary operations are associative, commutative and idempotent; they satisfy absorption and both distributive laws; $a\wedge 1=a$, $a\vee 0=a$, $a\wedge 0=0$ and $a\vee 1=1$. Its order is $a\le b$ if $a\wedge b=a$, equivalently $a\vee b=b$.

The algebra is nonempty because its bounds are elements. We allow $0=1$, in which case every $a$ equals $a\wedge 1=a\wedge 0=0$. This one-element algebra is called trivial. Otherwise the algebra is nontrivial. The empty join is $0$ and the empty meet is $1$.

All Boolean homomorphisms in this development preserve both bounds, as well as the operations.