thus multiples 1 c= INT ; :: according to XBOOLE_0:def 10 :: thesis: INT c= multiples 1
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in INT or x in multiples 1 )
assume x in INT ; :: thesis: x in multiples 1
then reconsider x = x as Integer ;
x is Multiple of 1 by Def15, INT_2:12;
hence x in multiples 1 ; :: thesis: verum