for A being Category
for a being Object of A holds 1Cat (a,(id a)) is Subcategory of A