theorem :: GLIB_000:129

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