theorem Th3: :: CHAIN_1:3

for x, y being object holds
( {x,y} is trivial iff x = y )