let H, F 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 ) by Def15;
then ( H = (Var1 H) '=' (Var2 H) or H = (Var1 H) 'in' (Var2 H) ) by Th53, Th54;
hence not F is_proper_subformula_of H by Th88, Th89; :: thesis: verum