theorem Th43: :: SUBLEMMA:43

for Al being QC-alphabet
for k being Nat
for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al holds still_not-bound_in (P ! ll) = Bound_Vars (P ! ll)