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