set M = { m where m is Multiple of i : verum } ;
{ m where m is Multiple of i : verum } c= INT

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { m where m is Multiple of i : verum } or x in INT )
assume x in { m where m is Multiple of i : verum } ; :: thesis: x in INT
then ex m being Multiple of i st x = m ;
hence x in INT by INT_1:def 2; :: thesis: verum

end;

hence { m where m is Multiple of i : verum } is Subset of INT ; :: thesis: verum