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