let Al be QC-alphabet ; :: thesis: still_not-bound_in (VERUM Al) c= Bound_Vars (VERUM Al)
Bound_Vars (VERUM Al) = {} by SUBSTUT1:2;
hence still_not-bound_in (VERUM Al) c= Bound_Vars (VERUM Al) by QC_LANG3:3; :: thesis: verum