for x, y being object st {x} c= {y} holds
x = y by Th3;