theorem :: ZF_LANG1:51

for H being ZF-formula
for x being Variable holds
( All (x,('not' H)) is_proper_subformula_of Ex (x,H) & 'not' H is_proper_subformula_of Ex (x,H) )