let F, H be Element of QC-WFF ; :: thesis: ( 'not' F is_subformula_of H implies F is_proper_subformula_of H )
F is_proper_subformula_of 'not' F by Th86;
hence ( 'not' F is_subformula_of H implies F is_proper_subformula_of H ) by Th83; :: thesis: verum