let n be Nat; :: thesis: ( n is even iff n mod 2 = 0 )
thus ( n is even implies n mod 2 = 0 ) :: thesis: ( n mod 2 = 0 implies n is even )

proof

assume n is even ; :: thesis: n mod 2 = 0
then consider k being Nat such that
A1: n = 2 * k by ABIAN:def 2;
n = (2 * k) + 0 by A1;
hence n mod 2 = 0 by NAT_D:def 2; :: thesis: verum

end;

assume n mod 2 = 0 ; :: thesis: n is even
then ex k being Nat st
( n = (2 * k) + 0 & 0 < 2 ) by NAT_D:def 2;
hence n is even ; :: thesis: verum