theorem Th28: :: ALTCAT_2:28

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