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