theorem :: ZF_LANG:86

for H being ZF-formula st H is negative holds
Subformulae H = (Subformulae (the_argument_of H)) \/ {H}