reconsider D = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) as SubCatStr of C by ALTCAT_2:def 11;
reconsider D = D as non empty full id-inheriting SubCatStr of C by Th34, Th35;
take D ; :: thesis: ( D is full & not D is empty & D is strict )
thus ( D is full & not D is empty & D is strict ) ; :: thesis: verum