:: deftheorem defines addint GR_CY_1:def 1 :
for b₁ being Element of bool [:[:INT,INT:],INT:] holds
( b₁ = addint iff for i1, i2 being Element of INT holds b₁ . (i1,i2) = addreal . (i1,i2) );