let G2 be removeLoops of G; :: thesis: G2 is loopless
assume not G2 is loopless ; :: thesis: contradiction
then consider v being object such that
A1: ex e being object st e Joins v,v,G2 by GLIB_000:18;
consider e being object such that
A2: e Joins v,v,G2 by A1;
v is set by TARSKI:1;
then e Joins v,v,G by A2, GLIB_000:72;
then e in G .loops() by Def2;
then not e in (the_Edges_of G) \ (G .loops()) by XBOOLE_0:def 5;
then not e in the_Edges_of G2 by GLIB_000:53;
hence contradiction by A2, GLIB_000:def 13; :: thesis: verum