let G2 be spanning Subgraph of G; :: thesis: not G2 is loopfull
assume A1: G2 is loopfull ; :: thesis: contradiction

now :: thesis: for v being Vertex of G ex e being object st e Joins v,v,G

let v be Vertex of G; :: thesis: ex e being object st e Joins v,v,G
v is Vertex of G2 by GLIB_000:def 33;
then consider e being object such that
A2: e Joins v,v,G2 by A1;
take e = e; :: thesis: e Joins v,v,G
thus e Joins v,v,G by A2, GLIB_000:72; :: thesis: verum

end;

hence contradiction by Def1; :: thesis: verum