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