:: deftheorem defines integer ZMATRLIN:def 2 :
for M being Matrix of REAL holds
( M is integer iff M is Matrix of INT );