for C being category
for B being non empty subcategory of C
for A being non empty subcategory of B holds A is non empty subcategory of C