let S be 1-sorted ; :: thesis: ( S is trivial implies S is good )
assume Z: S is trivial ; :: thesis: S is good
assume not S is good ; :: thesis: contradiction
then A1: the carrier of S = NAT by Def2;
the carrier of S is trivial by Z;
hence contradiction by A1; :: thesis: verum