reconsider X = {0,1,2} as non empty set ;
consider a1 being Element of X, k being Element of NAT such that
A1: a = [a1,k] by DOMAIN_1:9;
( a1 = 0 or a1 = 1 or a1 = 2 ) by ENUMSET1:def 1;
hence a `1 is Element of NAT by A1, MCART_1:7; :: thesis: verum