:: deftheorem Def5 defines addLoops GLIB_012:def 5 :
for G being _Graph
for V being set
for b₃ being Supergraph of G holds
( ( V c= the_Vertices_of G implies ( b₃ is addLoops of G,V iff ( the_Vertices_of b₃ = 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 b₃ = (the_Edges_of G) \/ E & dom f = E & rng f = V & the_Source_of b₃ = (the_Source_of G) +* f & the_Target_of b₃ = (the_Target_of G) +* f ) ) ) ) & ( not V c= the_Vertices_of G implies ( b₃ is addLoops of G,V iff b₃ == G ) ) );