let A be QC-alphabet ; :: thesis: for F being Element of QC-WFF A holds not F is_proper_subformula_of VERUM A
let F be Element of QC-WFF A; :: thesis: not F is_proper_subformula_of VERUM A
assume F is_proper_subformula_of VERUM A ; :: thesis: contradiction
then consider G being Element of QC-WFF A such that
A1: G is_immediate_constituent_of VERUM A by Th55;
thus contradiction by A1, Th41; :: thesis: verum