:: deftheorem defines without_fixpoints ABCMIZ_0:def 7 :
for A being AdjectiveStr holds
( A is without_fixpoints iff for a being adjective of A holds not non- a = a );