theorem :: ZF_LANG:85

for H being ZF-formula holds
( H is atomic iff Subformulae H = {H} )