for i being Integer holds
( i is even iff ex j being Integer st i = 2 * j ) by Lm1;