for Al being QC-alphabet
for s being QC-formula of Al
for x, y being bound_QC-variable of Al st s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x is valid holds
s . y is valid by Th10;