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