let G2 be _Graph; :: thesis: for V being set
for G1 being addVertices of G2,V st V \ (the_Vertices_of G2) <> {} holds
not G1 is loopfull
let V be set ; :: thesis: for G1 being addVertices of G2,V st V \ (the_Vertices_of G2) <> {} holds
not G1 is loopfull
let G1 be addVertices of G2,V; :: thesis: ( V \ (the_Vertices_of G2) <> {} implies not G1 is loopfull )
assume V \ (the_Vertices_of G2) <> {} ; :: thesis: not G1 is loopfull
then consider v being object such that
A1: v in V \ (the_Vertices_of G2) by XBOOLE_0:def 1;
reconsider v = v as Vertex of G1 by A1, GLIB_006:86;
v .edgesInOut() = {} by A1, GLIB_006:88, GLIB_000:def 49;
then for e being object holds not e Joins v,v,G1 by GLIB_000:62;
hence not G1 is loopfull ; :: thesis: verum