for H being ZF-formula holds H in Subformulae H