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

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