theorem Th64: :: ZF_LANG:64

for F, G, H being ZF-formula st F is_proper_subformula_of G & G is_proper_subformula_of H holds
F is_proper_subformula_of H