for M, N being non empty Reflexive MetrStruct holds max-Prod2 (M,N) is Reflexive