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

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