:: deftheorem defines non- ABCMIZ_0:def 5 :
for A being AdjectiveStr
for a being Element of the adjectives of A holds non- a = the non-op of A . a;