the carrier of (max-Prod2 M,N) = [:the carrier of M,the carrier of N:] by Def1;
hence not the carrier of (max-Prod2 M,N) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum