theorem Th9: :: NECKLACE:10

for a, b, c, d being set holds
not ( ( a = b implies c = d ) & ( c = d implies a = b ) & not ((a,b) --> (c,d)) " = (c,d) --> (a,b) )