theorem Th31: :: ALTCAT_2:31

for C being non empty AltCatStr
for D being non empty SubCatStr of C
for o1, o2 being Object of C
for p1, p2 being Object of D st o1 = p1 & o2 = p2 holds
<^p1,p2^> c= <^o1,o2^>