for H being ZF-formula holds H is_subformula_of H