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