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 full & D is strict )

thus the Arrows of D = the Arrows of C || the carrier of D ; :: according to ALTCAT_2:def 13 :: thesis: D is strict

thus D is strict ; :: thesis: verum

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 full & D is strict )

thus the Arrows of D = the Arrows of C || the carrier of D ; :: according to ALTCAT_2:def 13 :: thesis: D is strict

thus D is strict ; :: thesis: verum