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

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

end;

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