for i, j, n being Nat st n = max (i,j) holds
square-uparrow n c= (square-uparrow i) /\ (square-uparrow j)