A1: k in NAT by ORDINAL1:def 12;
6 in {6} by TARSKI:def 1;
hence [6,k] is free_QC-variable of A by ZFMISC_1:def 2, A1; :: thesis: verum