theorem Th47: :: YELLOW20:47

for A being non empty transitive AltCatStr
for B being non empty transitive SubCatStr of A holds B opp is SubCatStr of A opp