:: deftheorem defines compint BINOP_2:def 19 :
for b₁ being UnOp of INT holds
( b₁ = compint iff for i being Integer holds b₁ . i = - i );