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