theorem Th27: :: GRCAT_1:27

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