theorem :: ZF_LANG1:42

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