for n being Nat holds [n,n] in square-uparrow n