let G2 be _Graph; 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; 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 ; 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; ( 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 )
; 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
; verum