for i, j being Integer holds
( ( i is even iff j is even ) iff i - j is even ) ;