theorem Th9: :: IDEA_1:9

for n being Nat
for x, y, z being Tuple of n, BOOLEAN holds (x 'xor' y) 'xor' z = x 'xor' (y 'xor' z)