[x,y] is Element of (max-Prod2 M,N) by Def1;
hence [x,y] is Element of (max-Prod2 M,N) ; :: thesis: verum