theorem Th26: :: YELLOW20:26

for A being non empty AltCatStr
for B being non empty SubCatStr of A holds
( B is full iff for a1, a2 being Object of A
for b1, b2 being Object of B st b1 = a1 & b2 = a2 holds
<^b1,b2^> = <^a1,a2^> )