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