:: deftheorem defines even ABIAN:def 2 :
for n being Nat holds
( n is even iff ex k being Nat st n = 2 * k );