the carrier of (Trivial-Mem N) = {0} by Def1;
hence the carrier of (Trivial-Mem N) is 1 -element ; :: according to STRUCT_0:def 19 :: thesis: verum