theorem Th63: :: ZF_LANG:63

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