let G2 be _Graph; :: thesis: for V being set
for G1 being addLoops of G2,V
for e, v, w being object st v <> w holds
( e DJoins v,w,G1 iff e DJoins v,w,G2 )
let V be set ; :: thesis: for G1 being addLoops of G2,V
for e, v, w being object st v <> w holds
( e DJoins v,w,G1 iff e DJoins v,w,G2 )
let G1 be addLoops of G2,V; :: thesis: for e, v, w being object st v <> w holds
( e DJoins v,w,G1 iff e DJoins v,w,G2 )

per cases ( V c= the_Vertices_of G2 or not V c= the_Vertices_of G2 ) ;

suppose V c= the_Vertices_of G2 ; :: thesis: for e, v, w being object st v <> w holds
( e DJoins v,w,G1 iff e DJoins v,w,G2 )

then 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;
let e, v, w be object ; :: thesis: ( v <> w implies ( e DJoins v,w,G1 iff e DJoins v,w,G2 ) )
assume A2: v <> w ; :: thesis: ( e DJoins v,w,G1 iff e DJoins v,w,G2 )

hereby :: thesis: ( e DJoins v,w,G2 implies e DJoins v,w,G1 )

assume A3: e DJoins v,w,G1 ; :: thesis: e DJoins v,w,G2
then A4: e in (the_Edges_of G2) \/ E by A1, GLIB_000:def 14;
not e in E

proof

assume A5: e in E ; :: thesis: contradiction
then A6: (the_Source_of G1) . e = f . e by A1, FUNCT_4:13;
(the_Target_of G1) . e = f . e by A1, A5, FUNCT_4:13;
then ( f . e = v & f . e = w ) by A3, A6, GLIB_000:def 14;
hence contradiction by A2; :: thesis: verum

end;

then e in the_Edges_of G2 by A1, A4, XBOOLE_0:5;
hence e DJoins v,w,G2 by A3, GLIB_006:71; :: thesis: verum

end;

assume A7: e DJoins v,w,G2 ; :: thesis: e DJoins v,w,G1
( v is set & w is set ) by TARSKI:1;
hence e DJoins v,w,G1 by A7, GLIB_006:70; :: thesis: verum

end;

suppose not V c= the_Vertices_of G2 ; :: thesis: for e, v, w being object st v <> w holds
( e DJoins v,w,G1 iff e DJoins v,w,G2 )

then G1 == G2 by Def5;
hence for e, v, w being object st v <> w holds
( e DJoins v,w,G1 iff e DJoins v,w,G2 ) by GLIB_000:88; :: thesis: verum

end;

end;