let G1 be addLoops of G; :: thesis: G1 is loopfull
let v be Vertex of G1; :: according to GLIB_012:def 1 :: thesis: ex e being object st e Joins v,v,G1
consider E being set , f being one-to-one Function such that
A1: ( E misses the_Edges_of G & the_Edges_of G1 = (the_Edges_of G) \/ E & dom f = E & rng f = the_Vertices_of G & the_Source_of G1 = (the_Source_of G) +* f & the_Target_of G1 = (the_Target_of G) +* f ) by Def5;
v in the_Vertices_of G1 ;
then v in the_Vertices_of G by Th15;
then consider e being object such that
A2: ( e in dom f & f . e = v ) by A1, FUNCT_1:def 3;
take e ; :: thesis: e Joins v,v,G1
A3: ( (the_Source_of G1) . e = f . e & (the_Target_of G1) . e = f . e ) by A1, A2, FUNCT_4:13;
e in the_Edges_of G1 by A1, A2, XBOOLE_0:def 3;
hence e Joins v,v,G1 by A2, A3, GLIB_000:def 13; :: thesis: verum