[(In (i,INT)),(In (j,INT))] in [:INT,INT:] by ZFMISC_1:87;
hence In ([i,j],[:INT,INT:]) = [i,j] by SUBSET_1:def 8; :: thesis: verum