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: now

assume F is_proper_subformula_of G ; :: thesis: ( G is_subformula_of H implies F is_proper_subformula_of H )
then A2: ( F is_subformula_of G & len F < len G ) by ZF_LANG:83, ZF_LANG:def 41;
assume G is_subformula_of H ; :: thesis: F is_proper_subformula_of H
then ( F is_subformula_of H & len G <= len H ) by A2, Th43, ZF_LANG:86;
hence F is_proper_subformula_of H by A2, ZF_LANG:def 41; :: thesis: verum

end;

A3: now

assume A4: ( F is_subformula_of G & 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 )
then ( G is_subformula_of H & len F <= len G & len G < len H ) by Th43, ZF_LANG:83, ZF_LANG:def 41;
then ( F is_subformula_of H & len F < len H ) by A4, XXREAL_0:2, ZF_LANG:86;
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 ZF_LANG:def 41; :: thesis: verum

end;

( ( G is_immediate_constituent_of H implies G is_proper_subformula_of H ) & ( F is_immediate_constituent_of G implies F is_proper_subformula_of G ) ) by ZF_LANG:82;
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 A1, A3, ZF_LANG:85; :: thesis: verum