for C being category holds AllIso C is non empty subcategory of AllRetr C