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

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, ZF_LANG:def 41;
then A6: F is_subformula_of H by A5, ZF_LANG:65;
len G <= len H by A5, Th43;
hence F is_proper_subformula_of H by A4, A6, ZF_LANG:def 41; :: thesis: verum

end;

A7: now

assume that
A8: F is_subformula_of G and
A9: G is_proper_subformula_of H ; :: 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 )
G is_subformula_of H by A9, ZF_LANG:def 41;
then A10: F is_subformula_of H by A8, ZF_LANG:65;
len F <= len G by A8, Th43;
then len F < len H by A9, XXREAL_0:2, ZF_LANG:62;
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 A10, ZF_LANG:def 41; :: 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, A7, A1, ZF_LANG:64; :: thesis: verum