theorem :: GLIB_000:125

for G being _Graph
for e, x1, y1, x2, y2 being object st e DJoins x1,y1,G & e DJoins x2,y2,G holds
( x1 = x2 & y1 = y2 ) ;