4 in {4,5,6} by ENUMSET1:def 1;
then {4} c= {4,5,6} by ZFMISC_1:37;
hence [:{4},NAT :] is Subset of QC-variables by ZFMISC_1:118; :: thesis: verum