let G2 be _Graph; :: thesis: for v being Vertex of G2
for e, w being object
for G1 being addAdjVertex of G2,v,e,w st not e in the_Edges_of G2 & not w in the_Vertices_of G2 holds
not G1 is loopfull
let v be Vertex of G2; :: thesis: for e, w being object
for G1 being addAdjVertex of G2,v,e,w st not e in the_Edges_of G2 & not w in the_Vertices_of G2 holds
not G1 is loopfull
let e, w be object ; :: thesis: for G1 being addAdjVertex of G2,v,e,w st not e in the_Edges_of G2 & not w in the_Vertices_of G2 holds
not G1 is loopfull
let G1 be addAdjVertex of G2,v,e,w; :: thesis: ( not e in the_Edges_of G2 & not w in the_Vertices_of G2 implies not G1 is loopfull )
assume A1: ( not e in the_Edges_of G2 & not w in the_Vertices_of G2 ) ; :: thesis: not G1 is loopfull
then reconsider w = w as Vertex of G1 by GLIB_006:129;
v <> w by A1;
then for e being object holds not e Joins w,w,G1 by A1, GLIB_006:133;
hence not G1 is loopfull ; :: thesis: verum