( 6 in {6} & k in NAT ) by TARSKI:def 1;
hence [6,k] is free_QC-variable by ZFMISC_1:def 2; :: thesis: verum