let G1 be addLoops of G,V; :: thesis: not G1 is edge-finite
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 ) and
A2: ( dom f = E & rng f = V ) and
( the_Source_of G1 = (the_Source_of G) +* f & the_Target_of G1 = (the_Target_of G) +* f ) by GLIB_012:def 5;
E is infinite by A2, FINSET_1:8;
hence not G1 is edge-finite by A1; :: thesis: verum