theorem Th61: :: ABCMIZ_1:61

for C being initialized ConstructorSignature
for a being negative expression of C, an_Adj C ex a9 being positive expression of C, an_Adj C st
( a = (non_op C) term a9 & Non a = a9 )