theorem :: QC_LANG3:2

for A being QC-alphabet
for l being FinSequence of QC-variables A holds still_not-bound_in l = variables_in (l,(bound_QC-variables A)) ;