for G, H being ZF-formula holds
( not G is_proper_subformula_of H or not H is_immediate_constituent_of G )