let G2 be _Graph; :: thesis: for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st G2 is loopless & v1 <> v2 holds
G1 is loopless
let v1, v2 be Vertex of G2; :: thesis: for e being object
for G1 being addEdge of G2,v1,e,v2 st G2 is loopless & v1 <> v2 holds
G1 is loopless
let e be object ; :: thesis: for G1 being addEdge of G2,v1,e,v2 st G2 is loopless & v1 <> v2 holds
G1 is loopless
let G1 be addEdge of G2,v1,e,v2; :: thesis: ( G2 is loopless & v1 <> v2 implies G1 is loopless )
assume that
A1: G2 is loopless and
A2: v1 <> v2 ; :: thesis: G1 is loopless

per cases ( e in the_Edges_of G2 or not e in the_Edges_of G2 ) ;

suppose e in the_Edges_of G2 ; :: thesis: G1 is loopless

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

end;

suppose A3: not e in the_Edges_of G2 ; :: thesis: G1 is loopless

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: contradiction

per cases ( e1 in the_Edges_of G2 or not e1 in the_Edges_of G2 ) ;

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

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: verum

end;

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

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: verum

end;

end;

end;

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

end;

end;