theorem Th23: :: ALTCAT_2:23

for C being non empty AltCatStr
for o being Object of C
for o9 being Object of (ObCat o) holds o9 = o