theorem :: ZF_LANG1:54

for H being ZF-formula holds H in Subformulae H