theorem :: ZF_LANG1:41

for H being ZF-formula holds not H is_immediate_constituent_of H