:: deftheorem Def5 defines CQCSub_All SUBLEMMA:def 5 :
for Al being QC-alphabet
for B being CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
for SQ being second_Q_comp of B st B is quantifiable holds
CQCSub_All (B,SQ) = Sub_All (B,SQ);