let G2 be _Graph; :: thesis: for v being Vertex of G2
for e being object
for G1 being addEdge of G2,v,e,v st ( not G2 is loopless or not e in the_Edges_of G2 ) holds
not G1 is loopless
let v be Vertex of G2; :: thesis: for e being object
for G1 being addEdge of G2,v,e,v st ( not G2 is loopless or not e in the_Edges_of G2 ) holds
not G1 is loopless
let e be object ; :: thesis: for G1 being addEdge of G2,v,e,v st ( not G2 is loopless or not e in the_Edges_of G2 ) holds
not G1 is loopless
let G1 be addEdge of G2,v,e,v; :: thesis: ( ( not G2 is loopless or not e in the_Edges_of G2 ) implies not G1 is loopless )
assume ( not G2 is loopless or not e in the_Edges_of G2 ) ; :: thesis: not G1 is loopless

per cases then ( not G2 is loopless or not e in the_Edges_of G2 ) ;

suppose not G2 is loopless ; :: thesis: not G1 is loopless

hence not G1 is loopless ; :: thesis: verum

end;

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

then e DJoins v,v,G1 by Th109;
then ( e in the_Edges_of G1 & (the_Source_of G1) . e = v & (the_Target_of G1) . e = v ) by GLIB_000:def 14;
hence not G1 is loopless by GLIB_000:def 18; :: thesis: verum

end;

end;