theorem :: YELLOW20:43

for A being category
for B being non empty subcategory of A holds B,B are_isomorphic_under id A