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:23;
then ex k being Nat st
( n = (2 * k) + 0 & 0 < 2 ) by NAT_D:def 2;
hence 2 divides n by NAT_D:def 3; :: thesis: verum

end;

( 2 divides n implies n is even )

proof

assume 2 divides n ; :: thesis: n is even
then ex k being Nat st n = 2 * k by NAT_D:def 3;
hence n is even ; :: thesis: verum

end;

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