theorem Th12: :: ALTCAT_1:18

for C being non empty with_units AltCatStr
for o being Object of C holds <^o,o^> <> {}