let A be QC-alphabet ; :: thesis: Bound_Vars (VERUM A) = {}
Bound_Vars (VERUM A) = {} (bound_QC-variables A) by Lm1;
hence Bound_Vars (VERUM A) = {} ; :: thesis: verum