CatStr(# O,(Morphs O),(dom O),(cod O),(comp O),(ID O) #) is_full_subcategory_of C by CAT_2:21;
hence CatStr(# O,(Morphs O),(dom O),(cod O),(comp O),(ID O) #) is Subcategory of C by CAT_2:def 6; :: thesis: verum