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