theorem :: ZF_LANG1:44

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