for C being Category
for I being Indexing of C
for D being Categorial Category holds
( rng I is Subcategory of D iff D is TargetCat of I )