theorem Th28: :: FUNCTOR0:28

for A being non empty AltCatStr
for B being non empty SubCatStr of A
for o1, o2 being Object of B holds <^o1,o2^> c= <^((incl B) . o1),((incl B) . o2)^>