:: deftheorem defines incl CAT_2:def 5 :
for C being Category
for E being Subcategory of C holds incl E = id E;