let G1 be _trivial Cycle-like _Graph; :: thesis: for v being Vertex of G1
for e being Edge of G1 ex G2 being _trivial edgeless _Graph st G1 is addEdge of G2,v,e,v
let v be Vertex of G1; :: thesis: for e being Edge of G1 ex G2 being _trivial edgeless _Graph st G1 is addEdge of G2,v,e,v
let e be Edge of G1; :: thesis: ex G2 being _trivial edgeless _Graph st G1 is addEdge of G2,v,e,v
take G2 = the removeEdge of G1,e; :: thesis: G1 is addEdge of G2,v,e,v
set u = (the_Source_of G1) . e;
set w = (the_Target_of G1) . e;
( (the_Source_of G1) . e = v & (the_Target_of G1) . e = v ) by ZFMISC_1:def 10;
hence G1 is addEdge of G2,v,e,v by GLIB_008:37; :: thesis: verum