theorem Th9: :: INT_1:9

for i1, i2 being Integer holds
( i1 * i2 = 1 iff ( ( i1 = 1 & i2 = 1 ) or ( i1 = - 1 & i2 = - 1 ) ) )