set D = AltCatStr(# the carrier of C,the Arrows of C,the Comp of C #);
reconsider D = AltCatStr(# the carrier of C,the Arrows of C,the Comp of C #) as SubCatStr of C by Def11;
take D ; :: thesis: D is strict
thus D is strict ; :: thesis: verum