let G be _Graph; :: thesis: for e, x1, y1, x2, y2 being object st e DJoins x1,y1,G & e DJoins x2,y2,G holds
( x1 = x2 & y1 = y2 )
let e, x1, y1, x2, y2 be object ; :: thesis: ( e DJoins x1,y1,G & e DJoins x2,y2,G implies ( x1 = x2 & y1 = y2 ) )
assume A1: ( e DJoins x1,y1,G & e DJoins x2,y2,G ) ; :: thesis: ( x1 = x2 & y1 = y2 )
then ( (the_Source_of G) . e = x1 & (the_Target_of G) . e = y1 ) by GLIB_000:def 14;
hence ( x1 = x2 & y1 = y2 ) by A1, GLIB_000:def 14; :: thesis: verum