let G2 be _trivial edgeless _Graph; :: thesis: for v being Vertex of G2
for e being object
for G1 being addEdge of G2,v,e,v holds G1 is Cycle-like
let v be Vertex of G2; :: thesis: for e being object
for G1 being addEdge of G2,v,e,v holds G1 is Cycle-like
let e be object ; :: thesis: for G1 being addEdge of G2,v,e,v holds G1 is Cycle-like
let G1 be addEdge of G2,v,e,v; :: thesis: G1 is Cycle-like
A1: the_Edges_of G1 = (the_Edges_of G2) \/ {e} by GLIB_006:def 11
.= {e} ;

now :: thesis: for e1, e2, v1, v2 being object st e1 DJoins v1,v2,G1 & e2 DJoins v1,v2,G1 holds
e1 = e2

let e1, e2, v1, v2 be object ; :: thesis: ( e1 DJoins v1,v2,G1 & e2 DJoins v1,v2,G1 implies e1 = e2 )
assume ( e1 DJoins v1,v2,G1 & e2 DJoins v1,v2,G1 ) ; :: thesis: e1 = e2
then ( e1 in the_Edges_of G1 & e2 in the_Edges_of G1 ) by GLIB_000:def 14;
hence e1 = e2 by A1, ZFMISC_1:def 10; :: thesis: verum

end;

then A2: G1 is non-Dmulti by GLIB_000:def 21;
not e in the_Edges_of G2 ;
then not G1 is loopless by GLIB_006:113;
hence G1 is Cycle-like by A2; :: thesis: verum