theorem Th27: :: FUNCTOR0:27

for A being non empty AltCatStr
for B being non empty SubCatStr of A
for o being Object of B holds (incl B) . o = o