let G2 be addVertices of G,V; :: thesis: G2 is loopless
for v, e being object holds not e Joins v,v,G2

proof

let v be object ; :: thesis: for e being object holds not e Joins v,v,G2
given e being object such that A2: e Joins v,v,G2 ; :: thesis: contradiction
e DJoins v,v,G2 by A2, GLIB_000:16;
then e DJoins v,v,G by Th89;
then e Joins v,v,G by GLIB_000:16;
hence contradiction by GLIB_000:18; :: thesis: verum

end;

hence G2 is loopless by GLIB_000:18; :: thesis: verum