let G be _Graph; for e, v, w being object st e DSJoins {v},{w},G holds
e DJoins v,w,G
let e, v, w be object ; ( e DSJoins {v},{w},G implies e DJoins v,w,G )
assume
e DSJoins {v},{w},G
; 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; verum