theorem Th8: :: NECKLACE:9

for a, b being set holds (a .--> b) " = b .--> a