hereby :: thesis: ( ex k being Element of NAT st n = 2 * k implies n is even )

assume n is even ; :: thesis: ex k being Element of NAT st n = 2 * k
then 2 divides n by Def1;
then consider k being Integer such that
A1: n = 2 * k by INT_1:def 3;
0 <= k by A1, NAT_1:2, XREAL_1:132;
then reconsider k = k as Element of NAT by INT_1:3;
take k = k; :: thesis: n = 2 * k
thus n = 2 * k by A1; :: thesis: verum

end;

thus ( ex k being Element of NAT st n = 2 * k implies n is even ) by Lm1; :: thesis: verum