set M = the Matrix of n,m,INT;
reconsider L = inttorealM the Matrix of n,m,INT as Matrix of n,m,REAL ;
take L ; :: thesis: L is integer
thus L is integer ; :: thesis: verum