let G be non edgeless _Graph; :: thesis: for e being Edge of G
for e0, v, w being object st e0 Joins v,w, createGraph e holds
e0 = e
let e be Edge of G; :: thesis: for e0, v, w being object st e0 Joins v,w, createGraph e holds
e0 = e
let e0, v, w be object ; :: thesis: ( e0 Joins v,w, createGraph e implies e0 = e )
assume e0 Joins v,w, createGraph e ; :: thesis: e0 = e
then ( e0 DJoins v,w, createGraph e or e0 DJoins w,v, createGraph e ) by GLIB_000:16;
hence e0 = e by Th15; :: thesis: verum