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