let H, F be Element of QC-WFF ; :: thesis: ( H is_immediate_constituent_of F implies len (@ H) < len (@ F) )
A1: ( F = VERUM or F is atomic or F is negative or F is conjunctive or F is universal ) by QC_LANG1:7;
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, Th58, Th64, Th65, Th66, Th67;
hence len (@ H) < len (@ F) by QC_LANG1:12, QC_LANG1:13, QC_LANG1:14; :: thesis: verum