let n be Nat; square-uparrow n is infinite Subset of [:NAT,NAT:]
assume
square-uparrow n is not infinite Subset of [:NAT,NAT:]
; 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
; verum