theorem Th82: :: ZF_LANG:82

for H being ZF-formula holds Subformulae ('not' H) = (Subformulae H) \/ {('not' H)}