theorem Th62: :: ABCMIZ_1:62
for C being initialized ConstructorSignature
for a being non positive expression of C, an_Adj C holds (non_op C) term (Non a) = a