let G be non edgeless _Graph; :: thesis: for e being Edge of G
for e0, v, w being object st e0 DJoins v,w, createGraph e holds
( e0 = e & v = (the_Source_of G) . e & w = (the_Target_of G) . e )
let e be Edge of G; :: thesis: for e0, v, w being object st e0 DJoins v,w, createGraph e holds
( e0 = e & v = (the_Source_of G) . e & w = (the_Target_of G) . e )
let e0, v, w be object ; :: thesis: ( e0 DJoins v,w, createGraph e implies ( e0 = e & v = (the_Source_of G) . e & w = (the_Target_of G) . e ) )
assume A1: e0 DJoins v,w, createGraph e ; :: thesis: ( e0 = e & v = (the_Source_of G) . e & w = (the_Target_of G) . e )
then e0 in the_Edges_of (createGraph e) by GLIB_000:def 14;
then e0 in {e} by Th13;
then A2: ( e0 = e & v is set & w is set ) by TARSKI:def 1, TARSKI:1;
then e DJoins v,w,G by A1, GLIB_000:72;
hence ( e0 = e & v = (the_Source_of G) . e & w = (the_Target_of G) . e ) by A2, GLIB_000:def 14; :: thesis: verum