theorem :: GLIB_000:16

for G being _Graph
for e, x, y being object holds
( e Joins x,y,G iff ( e DJoins x,y,G or e DJoins y,x,G ) ) ;