let G be _Graph; :: thesis: 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 ) )
let X, Y be set ; :: thesis: for e being object holds
( e SJoins X,Y,G iff ( e DSJoins X,Y,G or e DSJoins Y,X,G ) )
let e be object ; :: thesis: ( e SJoins X,Y,G iff ( e DSJoins X,Y,G or e DSJoins Y,X,G ) )
( e SJoins X,Y,G iff ( e in the_Edges_of G & ( ( (the_Source_of G) . e in X & (the_Target_of G) . e in Y ) or ( (the_Source_of G) . e in Y & (the_Target_of G) . e in X ) ) ) ) by GLIB_000:def 15;
hence ( e SJoins X,Y,G iff ( e DSJoins X,Y,G or e DSJoins Y,X,G ) ) by GLIB_000:def 16; :: thesis: verum