the carrier of (SingleMSS x) = {x} by Def1;
hence not the carrier of (SingleMSS x) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum