theorem Th61: :: CQC_THE3:61

for A being QC-alphabet
for k being Nat
for l being QC-variable_list of k,A
for a being free_QC-variable of A
for x being bound_QC-variable of A holds still_not-bound_in (Subst (l,(a .--> x))) c= (still_not-bound_in l) \/ {x}