let n be Nat; :: thesis: ( 2 divides n iff n is even )
A1: ( n is even implies 2 divides n )

proof

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

end;

thus ( 2 divides n iff n is even ) by A1; :: thesis: verum