let A be QC-alphabet ; :: thesis: for F, H being Element of QC-WFF A st H is_immediate_constituent_of F holds
H is_proper_subformula_of F
let F, H be Element of QC-WFF A; :: thesis: ( H is_immediate_constituent_of F implies H is_proper_subformula_of F )
assume A1: H is_immediate_constituent_of F ; :: thesis: H is_proper_subformula_of F
hence H is_subformula_of F by Th52; :: according to QC_LANG2:def 21 :: thesis: H <> F
assume H = F ; :: thesis: contradiction
then len (@ H) = len (@ F) ;
hence contradiction by A1, Th51; :: thesis: verum