reconsider i = i, j = j as Element of INT by INT_1:def 2;
[i,j] is Element of [:INT,INT:] ;
hence [i,j] is Element of [:INT,INT:] ; :: thesis: verum