reconsider a = a, b = b as Element of NAT by ORDINAL1:def 13;
[a,b] is Element of [:NAT ,NAT :] ;
hence [a,b] is Element of [:NAT ,NAT :] ; :: thesis: verum