let H be ZF-formula; :: thesis: H in Subformulae H
H is_subformula_of H by ZF_LANG:59;
hence H in Subformulae H by ZF_LANG:def 42; :: thesis: verum