let H be ZF-formula; :: thesis: not H is_immediate_constituent_of H
assume H is_immediate_constituent_of H ; :: thesis: contradiction
then H is_proper_subformula_of H by ZF_LANG:61;
hence contradiction ; :: thesis: verum