let i be Integer; :: thesis: ( i is even iff ex j being Integer st i = 2 * j )

hereby :: thesis: ( ex j being Integer st i = 2 * j implies i is even )

assume i is even ; :: thesis: ex j being Integer st i = 2 * j
then 2 divides i by Def1;
hence ex j being Integer st i = 2 * j by INT_1:def 3; :: thesis: verum

end;

assume ex j being Integer st i = 2 * j ; :: thesis: i is even
hence 2 divides i by INT_1:def 3; :: according to ABIAN:def 1 :: thesis: verum