theorem :: CARDFIL4:27

for i, j, k, l, n being Nat st [i,j] in square-uparrow n holds
( [(i + k),j] in square-uparrow n & [i,(j + l)] in square-uparrow n )