theorem :: GLIB_000:130

for G being _Graph
for X, Y being set
for e being object holds
( e SJoins X,Y,G iff ( e DSJoins X,Y,G or e DSJoins Y,X,G ) ) ;