theorem Th3: :: NATTRA_1:7
for A being Category
for a being Object of A holds 1Cat (a,(id a)) is Subcategory of A