let G, H be ZF-formula; :: thesis: ( not G is_subformula_of H or not H is_immediate_constituent_of G )
assume ( G is_subformula_of H & H is_immediate_constituent_of G ) ; :: thesis: contradiction
then G is_proper_subformula_of G by Th40;
hence contradiction ; :: thesis: verum