let G2 be _Graph; :: thesis: for V being Subset of (the_Vertices_of G2)
for G1 being addLoops of G2,V
for v being Vertex of G1 st v in V holds
v,v are_adjacent
let V be Subset of (the_Vertices_of G2); :: thesis: for G1 being addLoops of G2,V
for v being Vertex of G1 st v in V holds
v,v are_adjacent
let G1 be addLoops of G2,V; :: thesis: for v being Vertex of G1 st v in V holds
v,v are_adjacent
let v be Vertex of G1; :: thesis: ( v in V implies v,v are_adjacent )
consider E being set , f being one-to-one Function such that
A1: ( E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & dom f = E & rng f = V & the_Source_of G1 = (the_Source_of G2) +* f & the_Target_of G1 = (the_Target_of G2) +* f ) by Def5;
assume v in V ; :: thesis: v,v are_adjacent
then consider e being object such that
A2: ( e in dom f & f . e = v ) by A1, FUNCT_1:def 3;
A3: (the_Source_of G1) . e = v by A1, A2, FUNCT_4:13;
A4: (the_Target_of G1) . e = v by A1, A2, FUNCT_4:13;
e in the_Edges_of G1 by A1, A2, XBOOLE_0:def 3;
then e Joins v,v,G1 by A3, A4, GLIB_000:def 13;
hence v,v are_adjacent by CHORD:def 3; :: thesis: verum