let G1 be addLoops of G,V; :: thesis: not G1 is loopless
consider E being set , f being one-to-one Function such that
A4: ( E misses the_Edges_of G & the_Edges_of G1 = (the_Edges_of G) \/ E & dom f = E & rng f = V & the_Source_of G1 = (the_Source_of G) +* f & the_Target_of G1 = (the_Target_of G) +* f ) by Def5;

now :: thesis: ex v, e being object st e DJoins v,v,G1

reconsider v = the Element of V as object ;
take v = v; :: thesis: ex e being object st e DJoins v,v,G1
consider e being object such that
A5: ( e in dom f & f . e = v ) by A4, FUNCT_1:def 3;
take e = e; :: thesis: e DJoins v,v,G1
A6: ( (the_Source_of G1) . e = f . e & (the_Target_of G1) . e = f . e ) by A4, A5, FUNCT_4:13;
e in the_Edges_of G1 by A4, A5, XBOOLE_0:def 3;
hence e DJoins v,v,G1 by A5, A6, GLIB_000:def 14; :: thesis: verum

end;

hence not G1 is loopless by GLIB_000:136; :: thesis: verum