set L = BooleLatt {};
the carrier of (BooleLatt {}) = bool {} by LATTICE3:def 1;
then BooleLatt {} is finite ;
hence ex b₁ being Lattice st b₁ is finite ; :: thesis: verum