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