let G2 be _Graph; :: thesis: for V being set
for G1 being addLoops of G2,V holds the_Vertices_of G1 = the_Vertices_of G2
let V be set ; :: thesis: for G1 being addLoops of G2,V holds the_Vertices_of G1 = the_Vertices_of G2
let G1 be addLoops of G2,V; :: thesis: the_Vertices_of G1 = the_Vertices_of G2

per cases ( V c= the_Vertices_of G2 or not V c= the_Vertices_of G2 ) ;

suppose V c= the_Vertices_of G2 ; :: thesis: the_Vertices_of G1 = the_Vertices_of G2

hence the_Vertices_of G1 = the_Vertices_of G2 by Def5; :: thesis: verum

end;

suppose not V c= the_Vertices_of G2 ; :: thesis: the_Vertices_of G1 = the_Vertices_of G2

then G1 == G2 by Def5;
hence the_Vertices_of G1 = the_Vertices_of G2 by GLIB_000:def 34; :: thesis: verum

end;

end;