let n be Nat; :: thesis: square-uparrow n is infinite Subset of [:NAT,NAT:]

assume square-uparrow n is not infinite Subset of [:NAT,NAT:] ; :: thesis: contradiction

then reconsider A = square-uparrow n as finite Subset of [:NAT,NAT:] ;

consider i, j being Nat such that

A1: A c= [:(Segm i),(Segm j):] by Th16;

consider k, l being Nat such that

k = [n,n] `1 and

l = [n,n] `2 and

A2: n <= k and

A3: n <= l ;

( k <= k + i & l <= l + j ) by NAT_1:11;

then A4: ( n <= k + i & n <= l + j ) by XXREAL_0:2, A2, A3;

( k + i in NAT & l + j in NAT ) by ORDINAL1:def 12;

then reconsider y = [(k + i),(l + j)] as Element of [:NAT,NAT:] by ZFMISC_1:def 2;

( y `1 = k + i & y `2 = l + j ) ;

then y in square-uparrow n by Def3, A4;

then ex a, b being object st

( a in Segm i & b in Segm j & y = [a,b] ) by A1, ZFMISC_1:def 2;

then ( k + i in Segm i & l + j in Segm j ) by XTUPLE_0:1;

then ( (k + i) - i < i - i & (l + j) - j < j - j ) by NAT_1:44, XREAL_1:14;

then ( k < 0 & l < 0 ) ;

hence contradiction ; :: thesis: verum

assume square-uparrow n is not infinite Subset of [:NAT,NAT:] ; :: thesis: contradiction

then reconsider A = square-uparrow n as finite Subset of [:NAT,NAT:] ;

consider i, j being Nat such that

A1: A c= [:(Segm i),(Segm j):] by Th16;

consider k, l being Nat such that

k = [n,n] `1 and

l = [n,n] `2 and

A2: n <= k and

A3: n <= l ;

( k <= k + i & l <= l + j ) by NAT_1:11;

then A4: ( n <= k + i & n <= l + j ) by XXREAL_0:2, A2, A3;

( k + i in NAT & l + j in NAT ) by ORDINAL1:def 12;

then reconsider y = [(k + i),(l + j)] as Element of [:NAT,NAT:] by ZFMISC_1:def 2;

( y `1 = k + i & y `2 = l + j ) ;

then y in square-uparrow n by Def3, A4;

then ex a, b being object st

( a in Segm i & b in Segm j & y = [a,b] ) by A1, ZFMISC_1:def 2;

then ( k + i in Segm i & l + j in Segm j ) by XTUPLE_0:1;

then ( (k + i) - i < i - i & (l + j) - j < j - j ) by NAT_1:44, XREAL_1:14;

then ( k < 0 & l < 0 ) ;

hence contradiction ; :: thesis: verum