theorem Th3: :: INT_8:3

for x being Integer
for X being Subset of INT
for a being Integer holds
( x in a ** X iff ex y being Integer st
( y in X & x = a * y ) )