theorem Th60: :: ABCMIZ_1:60

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