theorem ThMultTableINTGroup2: :: GROUP_24:79

for x, y being Element of (INT.Group 2) holds
( ( x = 0 implies x * y = y ) & ( y = 0 implies x * y = x ) & ( x = 1 & y = 1 implies x * y = 1_ (INT.Group 2) ) )