for i being Integer holds
( i is even iff i ^2 is even ) ;