:: deftheorem Def42 defines Subformulae ZF_LANG:def 42 :
for H being ZF-formula
for b₂ being set holds
( b₂ = Subformulae H iff for a being set holds
( a in b₂ iff ex F being ZF-formula st
( F = a & F is_subformula_of H ) ) );