:: deftheorem Def4 defines Subformula QC_LANG4:def 4 :
for A being QC-alphabet
for F, b₃ being Element of QC-WFF A holds
( b₃ is Subformula of F iff b₃ is_subformula_of F );