4 in {4} by TARSKI:def 1;
hence [4,k] is bound_QC-variable by ZFMISC_1:def 2; :: thesis: verum