theorem Th84: :: ZF_LANG:84

for x being Variable
for H being ZF-formula holds Subformulae (All (x,H)) = (Subformulae H) \/ {(All (x,H))}