for Al being QC-alphabet holds still_not-bound_in (VERUM Al) c= Bound_Vars (VERUM Al) by QC_LANG3:3;