let F, G, H be ZF-formula; :: thesis: ( ( ( F is_proper_subformula_of G & G is_subformula_of H ) or ( F is_subformula_of G & G is_proper_subformula_of H ) or ( F is_subformula_of G & G is_immediate_constituent_of H ) or ( F is_immediate_constituent_of G & G is_subformula_of H ) or ( F is_proper_subformula_of G & G is_immediate_constituent_of H ) or ( F is_immediate_constituent_of G & G is_proper_subformula_of H ) ) implies F is_proper_subformula_of H )
A1: ( F is_immediate_constituent_of G implies F is_proper_subformula_of G ) by ZF_LANG:61;
A2: now :: thesis: ( F is_proper_subformula_of G & G is_subformula_of H implies F is_proper_subformula_of H )
assume A3: F is_proper_subformula_of G ; :: thesis: ( G is_subformula_of H implies F is_proper_subformula_of H )
then A4: len F < len G by ZF_LANG:62;
assume A5: G is_subformula_of H ; :: thesis: F is_proper_subformula_of H
F is_subformula_of G by A3;
then A6: F is_subformula_of H by A5, ZF_LANG:65;
len G <= len H by A5, Th39;
hence F is_proper_subformula_of H by A4, A6; :: thesis: verum
end;
( G is_immediate_constituent_of H implies G is_proper_subformula_of H ) by ZF_LANG:61;
hence ( ( ( F is_proper_subformula_of G & G is_subformula_of H ) or ( F is_subformula_of G & G is_proper_subformula_of H ) or ( F is_subformula_of G & G is_immediate_constituent_of H ) or ( F is_immediate_constituent_of G & G is_subformula_of H ) or ( F is_proper_subformula_of G & G is_immediate_constituent_of H ) or ( F is_immediate_constituent_of G & G is_proper_subformula_of H ) ) implies F is_proper_subformula_of H ) by A2, A1; :: thesis: verum