1 in INT by INT_1:def 2;
then reconsider s = [1,1] as Element of [:INT,INT:] by ZFMISC_1:87;
take s ; :: thesis: s is positive
thus s is positive ; :: thesis: verum