let G be non edgeless _Graph; :: thesis: for e being Edge of G holds e DJoins (the_Source_of G) . e,(the_Target_of G) . e, createGraph e
let e be Edge of G; :: thesis: e DJoins (the_Source_of G) . e,(the_Target_of G) . e, createGraph e
A1: e DJoins (the_Source_of G) . e,(the_Target_of G) . e,G by GLIB_000:def 14;
the_Edges_of (createGraph e) = {e} by Th13;
then e in the_Edges_of (createGraph e) by TARSKI:def 1;
hence e DJoins (the_Source_of G) . e,(the_Target_of G) . e, createGraph e by A1, GLIB_000:73; :: thesis: verum