set M = the Matrix of INT;
reconsider L = inttorealM the Matrix of INT as Matrix of REAL ;
take L ; :: thesis: L is integer
thus L is Matrix of INT ; :: according to ZMATRLIN:def 2 :: thesis: verum