theorem Th70: :: ZF_LANG:70

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