theorem Th15: :: RINGCAT1:15

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