let A be QC-alphabet ; :: thesis: for F, H being Element of QC-WFF A st H is_immediate_constituent_of F holds
len (@ H) < len (@ F)
let F, H be Element of QC-WFF A; :: thesis: ( H is_immediate_constituent_of F implies len (@ H) < len (@ F) )
A1: ( F = VERUM A or F is atomic or F is negative or F is conjunctive or F is universal ) by QC_LANG1:9;
assume H is_immediate_constituent_of F ; :: thesis: len (@ H) < len (@ F)
then ( ( F is negative & H = the_argument_of F ) or ( F is conjunctive & H = the_left_argument_of F ) or ( F is conjunctive & H = the_right_argument_of F ) or ( F is universal & H = the_scope_of F ) ) by A1, Th41, Th47, Th48, Th49, Th50;
hence len (@ H) < len (@ F) by QC_LANG1:14, QC_LANG1:15, QC_LANG1:16; :: thesis: verum