let G be _Graph; :: thesis: for e, v, w being object st e DSJoins {v},{w},G holds

e DJoins v,w,G

let e, v, w be object ; :: thesis: ( e DSJoins {v},{w},G implies e DJoins v,w,G )

assume e DSJoins {v},{w},G ; :: thesis: e DJoins v,w,G

then ( e in the_Edges_of G & (the_Source_of G) . e in {v} & (the_Target_of G) . e in {w} ) by GLIB_000:def 16;

then ( e in the_Edges_of G & (the_Source_of G) . e = v & (the_Target_of G) . e = w ) by TARSKI:def 1;

hence e DJoins v,w,G by GLIB_000:def 14; :: thesis: verum

e DJoins v,w,G

let e, v, w be object ; :: thesis: ( e DSJoins {v},{w},G implies e DJoins v,w,G )

assume e DSJoins {v},{w},G ; :: thesis: e DJoins v,w,G

then ( e in the_Edges_of G & (the_Source_of G) . e in {v} & (the_Target_of G) . e in {w} ) by GLIB_000:def 16;

then ( e in the_Edges_of G & (the_Source_of G) . e = v & (the_Target_of G) . e = w ) by TARSKI:def 1;

hence e DJoins v,w,G by GLIB_000:def 14; :: thesis: verum