theorem LmDE311A: :: ZMODLAT3:23

for X being finite Subset of RAT ex a being Element of INT st
( a <> 0 & ( for r being Element of RAT st r in X holds
a * r in INT ) )