:: deftheorem defines negative ZF_LANG:def 12 :
for H being ZF-formula holds
( H is negative iff ex H1 being ZF-formula st H = 'not' H1 );