:: deftheorem Def36 defines Non ABCMIZ_1:def 36 :
for C being initialized ConstructorSignature
for a being expression of C, an_Adj C holds
( ( ex a9 being expression of C, an_Adj C st a = (non_op C) term a9 implies Non a = a | <*0*> ) & ( ( for a9 being expression of C, an_Adj C holds not a = (non_op C) term a9 ) implies Non a = (non_op C) term a ) );