for Al being QC-alphabet
for x, y being bound_QC-variable of Al
for s9 being QC-formula of Al st x <> y & not x in still_not-bound_in s9 holds
not x in still_not-bound_in (s9 . y)