:: deftheorem Def30 defines the_argument_of ZF_LANG:def 30 :
for H being ZF-formula st H is negative holds
for b₂ being ZF-formula holds
( b₂ = the_argument_of H iff 'not' b₂ = H );