theorem Th10: :: CQC_THE1:14

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for s being QC-formula of Al
for x, y being bound_QC-variable of Al st s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in Cn X holds
s . y in Cn X