fact: Definition subcategory_property a (obp morp:E->Prop) := (Category.axioms a) & (forall u v, mor a u -> mor a v -> source u = target v -> morp u -> morp v -> morp (comp a u v)) & (forall x, ob a x -> obp x -> morp (id a x)) & (forall u, mor a u -> morp u -> obp (source u)) & (forall u, mor a u -> morp u -> obp (target u)).
imports: Arith ordinal nat_trans