:: deftheorem Def28 defines incl FUNCTOR0:def 28 :
for A being AltCatStr
for B being SubCatStr of A
for b₃ being strict FunctorStr over B,A holds
( b₃ = incl B iff ( the ObjectMap of b₃ = id [: the carrier of B, the carrier of B:] & the MorphMap of b₃ = id the Arrows of B ) );