theorem Th4: :: FUNCTOR1:4

for A being non empty reflexive AltCatStr
for B being non empty reflexive SubCatStr of A
for C being non empty SubCatStr of A
for D being non empty SubCatStr of B st C = D holds
incl C = (incl B) * (incl D)