for R being Ring
for x, y1, y2 being object st GO x,y1,R & GO x,y2,R holds
y1 = y2