the carrier of (StoneSpace BL) = ultraset BL by Def8;
hence not the carrier of (StoneSpace BL) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum