theorem :: HILBERT3:2

for i being Integer holds
( i is odd iff i - 1 is even ) ;