:: deftheorem Def11 defines SubCatStr ALTCAT_2:def 11 :
for C, b₂ being AltCatStr holds
( b₂ is SubCatStr of C iff ( the carrier of b₂ c= the carrier of C & the Arrows of b₂ cc= the Arrows of C & the Comp of b₂ cc= the Comp of C ) );