let G be _Graph; :: thesis: G is addLoops of G, {}
A1: ( G is Supergraph of G & {} c= the_Vertices_of G ) by GLIB_006:61, XBOOLE_1:2;

now :: thesis: ( the_Vertices_of G = the_Vertices_of G & ex E being set ex f being one-to-one Function st
( E misses the_Edges_of G & the_Edges_of G = (the_Edges_of G) \/ E & dom f = E & rng f = {} & the_Source_of G = (the_Source_of G) +* f & the_Target_of G = (the_Target_of G) +* f ) )

thus the_Vertices_of G = the_Vertices_of G ; :: thesis: ex E being set ex f being one-to-one Function st
( E misses the_Edges_of G & the_Edges_of G = (the_Edges_of G) \/ E & dom f = E & rng f = {} & the_Source_of G = (the_Source_of G) +* f & the_Target_of G = (the_Target_of G) +* f )
reconsider E = {} as set ;
reconsider f = the empty Function as one-to-one Function ;
take E = E; :: thesis: ex f being one-to-one Function st
( E misses the_Edges_of G & the_Edges_of G = (the_Edges_of G) \/ E & dom f = E & rng f = {} & the_Source_of G = (the_Source_of G) +* f & the_Target_of G = (the_Target_of G) +* f )
take f = f; :: thesis: ( E misses the_Edges_of G & the_Edges_of G = (the_Edges_of G) \/ E & dom f = E & rng f = {} & the_Source_of G = (the_Source_of G) +* f & the_Target_of G = (the_Target_of G) +* f )
thus E misses the_Edges_of G by XBOOLE_1:65; :: thesis: ( the_Edges_of G = (the_Edges_of G) \/ E & dom f = E & rng f = {} & the_Source_of G = (the_Source_of G) +* f & the_Target_of G = (the_Target_of G) +* f )
thus the_Edges_of G = (the_Edges_of G) \/ E ; :: thesis: ( dom f = E & rng f = {} & the_Source_of G = (the_Source_of G) +* f & the_Target_of G = (the_Target_of G) +* f )
thus ( dom f = E & rng f = {} ) ; :: thesis: ( the_Source_of G = (the_Source_of G) +* f & the_Target_of G = (the_Target_of G) +* f )
thus the_Source_of G = (the_Source_of G) +* f by FUNCT_4:21; :: thesis: the_Target_of G = (the_Target_of G) +* f
thus the_Target_of G = (the_Target_of G) +* f by FUNCT_4:21; :: thesis: verum

end;

hence G is addLoops of G, {} by A1, Def5; :: thesis: verum