:: deftheorem defines even ABIAN:def 1 :
for i being Integer holds
( i is even iff 2 divides i );