let F, H be ZF-formula; :: thesis: ( 'not' F is_subformula_of H implies F is_proper_subformula_of H )
F is_immediate_constituent_of 'not' F ;
hence ( 'not' F is_subformula_of H implies F is_proper_subformula_of H ) by Th40; :: thesis: verum