:: deftheorem defines non_op ABCMIZ_1:def 16 :
for C being ConstructorSignature holds non_op C = non_op ;