let G2 be _Graph; :: thesis: for v being object
for V being Subset of (the_Vertices_of G2)
for G1 being addAdjVertexAll of G2,v,V st not v in the_Vertices_of G2 holds
not G1 is loopfull
let v be object ; :: thesis: for V being Subset of (the_Vertices_of G2)
for G1 being addAdjVertexAll of G2,v,V st not v in the_Vertices_of G2 holds
not G1 is loopfull
let V be Subset of (the_Vertices_of G2); :: thesis: for G1 being addAdjVertexAll of G2,v,V st not v in the_Vertices_of G2 holds
not G1 is loopfull
let G1 be addAdjVertexAll of G2,v,V; :: thesis: ( not v in the_Vertices_of G2 implies not G1 is loopfull )
assume A1: not v in the_Vertices_of G2 ; :: thesis: not G1 is loopfull
then reconsider v = v as Vertex of G1 by GLIB_007:50;
for e being object holds not e Joins v,v,G1 by A1, GLIB_007:def 4;
hence not G1 is loopfull ; :: thesis: verum