let a be Integer; :: thesis: for X being Subset of INT holds a ** X c= INT
let X be Subset of INT; :: thesis: a ** X c= INT
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in a ** X or x in INT )
assume A1: x in a ** X ; :: thesis: x in INT
then reconsider x9 = x as Real ;
consider y being Complex such that
A2: x9 = a * y and
A3: y in X by A1, MEMBER_1:195;
reconsider y9 = y as Integer by A3;
x9 = a * y9 by A2;
hence x in INT by INT_1:def 2; :: thesis: verum