the carrier of (BooleLatt X) = bool X by Def1;
hence not the carrier of (BooleLatt X) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum