let A be QC-alphabet ; :: thesis: for F, H being Element of QC-WFF A st 'not' F is_subformula_of H holds
F is_proper_subformula_of H
let F, H be Element of QC-WFF A; :: thesis: ( 'not' F is_subformula_of H implies F is_proper_subformula_of H )
F is_proper_subformula_of 'not' F by Th66;
hence ( 'not' F is_subformula_of H implies F is_proper_subformula_of H ) by Th63; :: thesis: verum