for C being category holds AllCoretr C is non empty subcategory of AllMono C