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

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