:: deftheorem Def22 defines Subformulae QC_LANG2:def 22 :
for A being QC-alphabet
for H being Element of QC-WFF A
for b₃ being set holds
( b₃ = Subformulae H iff for a being object holds
( a in b₃ iff ex F being Element of QC-WFF A st
( F = a & F is_subformula_of H ) ) );