let G2 be _Graph; :: thesis:
let v1, v2 be Vertex of G2; :: thesis:
let e be object ; :: thesis:
let G1 be addEdge of G2,v1,e,v2; :: thesis:
assume that
A1: G2 is loopless and
A2: v1 <> v2 ; :: thesis:

per cases ;

suppose e in the_Edges_of G2 ; :: thesis:

then G1 == G2 by Def11;
hence G1 is loopless by A1, GLIB_000:89; :: thesis:

end;

suppose A3: not e in the_Edges_of G2 ; :: thesis:

for e1 being object holds
( not e1 in the_Edges_of G1 or not (the_Source_of G1) . e1 = (the_Target_of G1) . e1 )

proof

given e1 being object such that A4: e1 in the_Edges_of G1 and
A5: (the_Source_of G1) . e1 = (the_Target_of G1) . e1 ; :: thesis:

per cases ;

suppose A6: e1 in the_Edges_of G2 ; :: thesis:

reconsider e1 = e1 as set by TARSKI:1;
( (the_Source_of G1) . e1 = (the_Source_of G2) . e1 & (the_Target_of G1) . e1 = (the_Target_of G2) . e1 ) by A6, Def9;
hence contradiction by A1, A5, A6, GLIB_000:def 18; :: thesis:

end;

suppose A7: not e1 in the_Edges_of G2 ; :: thesis:

the_Edges_of G1 = (the_Edges_of G2) \/ {e} by A3, Def11;
then e1 in {e} by A4, A7, XBOOLE_0:def 3;
then e1 = e by TARSKI:def 1;
then e1 DJoins v1,v2,G1 by A7, Th109;
then ( (the_Source_of G1) . e1 = v1 & (the_Target_of G1) . e1 = v2 ) by GLIB_000:def 14;
hence contradiction by A2, A5; :: thesis:

end;

end;

end;

hence G1 is loopless by GLIB_000:def 18; :: thesis:

end;

end;