theorem Th12: :: YELLOW18:12

for A, B being non empty transitive AltCatStr st A,B are_opposite & A is with_units holds
B is with_units