:: deftheorem defines Ex ZF_LANG:def 19 :
for x being Variable
for H being ZF-formula holds Ex (x,H) = 'not' (All (x,('not' H)));