theorem Th8: :: ABCMIZ_1:8

varcl {} = {}