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