:: deftheorem Def4 defines CQC-WFF-like SUBLEMMA:def 4 :
for Al being QC-alphabet
for B being Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):] holds
( B is CQC-WFF-like iff B `1 in CQC-Sub-WFF Al );