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 Joins v,w,G1 iff e Joins 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 Joins v,w,G1 iff e Joins v,w,G2 )
let G1 be addLoops of G2,V; :: thesis: for e, v, w being object st v <> w holds
( e Joins v,w,G1 iff e Joins v,w,G2 )
let e, v, w be object ; :: thesis: ( v <> w implies ( e Joins v,w,G1 iff e Joins v,w,G2 ) )
assume A1: v <> w ; :: thesis: ( e Joins v,w,G1 iff e Joins v,w,G2 )

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

assume e Joins v,w,G1 ; :: thesis: e Joins v,w,G2

per cases then ( e DJoins v,w,G1 or e DJoins w,v,G1 ) by GLIB_000:16;

suppose e DJoins v,w,G1 ; :: thesis: e Joins v,w,G2

then e DJoins v,w,G2 by A1, Th16;
hence e Joins v,w,G2 by GLIB_000:16; :: thesis: verum

end;

suppose e DJoins w,v,G1 ; :: thesis: e Joins v,w,G2

then e DJoins w,v,G2 by A1, Th16;
hence e Joins v,w,G2 by GLIB_000:16; :: thesis: verum

end;

end;

end;

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