let A be QC-alphabet ; :: thesis: for F, G being Element of QC-WFF A st F is_subformula_of G holds
len (@ F) <= len (@ G)
let F, G be Element of QC-WFF A; :: thesis: ( F is_subformula_of G implies len (@ F) <= len (@ G) )
assume A1: F is_subformula_of G ; :: thesis: len (@ F) <= len (@ G)

per cases ( F = G or F <> G ) ;

suppose F = G ; :: thesis: len (@ F) <= len (@ G)

hence len (@ F) <= len (@ G) ; :: thesis: verum

end;

suppose F <> G ; :: thesis: len (@ F) <= len (@ G)

then F is_proper_subformula_of G by A1, QC_LANG2:def 21;
hence len (@ F) <= len (@ G) by QC_LANG2:54; :: thesis: verum

end;

end;