let G be _Graph; :: thesis: for e, v, w being object st e SJoins {v},{w},G holds
e Joins v,w,G
let e, v, w be object ; :: thesis: ( e SJoins {v},{w},G implies e Joins v,w,G )
assume e SJoins {v},{w},G ; :: thesis: e Joins v,w,G
then ( e in the_Edges_of G & ( ( (the_Source_of G) . e in {v} & (the_Target_of G) . e in {w} ) or ( (the_Source_of G) . e in {w} & (the_Target_of G) . e in {v} ) ) ) by GLIB_000:def 15;
then ( e in the_Edges_of G & ( ( (the_Source_of G) . e = v & (the_Target_of G) . e = w ) or ( (the_Source_of G) . e = w & (the_Target_of G) . e = v ) ) ) by TARSKI:def 1;
hence e Joins v,w,G by GLIB_000:def 13; :: thesis: verum