let F, H be ZF-formula; :: thesis: ( H is atomic implies not F is_proper_subformula_of H )
assume H is atomic ; :: thesis: not F is_proper_subformula_of H
then ( H is being_equality or H is being_membership ) ;
then ( H = (Var1 H) '=' (Var2 H) or H = (Var1 H) 'in' (Var2 H) ) by Th36, Th37;
hence not F is_proper_subformula_of H by Th67, Th68; :: thesis: verum