theorem :: CQC_THE1:58

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 . y in CQC-WFF Al & not x in still_not-bound_in s & X |- s . x holds
X |- s . y by Th10;