let n be Nat; :: thesis: [n,n] in square-uparrow n
n in NAT by ORDINAL1:def 12;
then reconsider x = [n,n] as Element of [:NAT,NAT:] by ZFMISC_1:def 2;
( x `1 = n & x `2 = n ) ;
hence [n,n] in square-uparrow n by Def3; :: thesis: verum