let S be non empty 1-sorted ; :: thesis: ( S is trivial implies S is good )
assume S is trivial ; :: thesis: S is good
then reconsider T = S as non empty trivial 1-sorted ;
assume not S is good ; :: thesis: contradiction
then A1: ( the carrier of S = NAT or the carrier of S = SCM-Instr S ) by Def2;
the carrier of T is trivial ;
hence contradiction by A1; :: thesis: verum