let G be _Graph; :: thesis: for v being object
for V being set
for G1 being addAdjVertexToAll of G,v,V
for G2 being addAdjVertexFromAll of G,v,V
for v1, e, v2 being object holds
( e Joins v1,v2,G1 iff e Joins v1,v2,G2 )
let v be object ; :: thesis: for V being set
for G1 being addAdjVertexToAll of G,v,V
for G2 being addAdjVertexFromAll of G,v,V
for v1, e, v2 being object holds
( e Joins v1,v2,G1 iff e Joins v1,v2,G2 )
let V be set ; :: thesis: for G1 being addAdjVertexToAll of G,v,V
for G2 being addAdjVertexFromAll of G,v,V
for v1, e, v2 being object holds
( e Joins v1,v2,G1 iff e Joins v1,v2,G2 )
let G1 be addAdjVertexToAll of G,v,V; :: thesis: for G2 being addAdjVertexFromAll of G,v,V
for v1, e, v2 being object holds
( e Joins v1,v2,G1 iff e Joins v1,v2,G2 )
let G2 be addAdjVertexFromAll of G,v,V; :: thesis: for v1, e, v2 being object holds
( e Joins v1,v2,G1 iff e Joins v1,v2,G2 )

per cases ( ( V c= the_Vertices_of G & not v in the_Vertices_of G ) or not V c= the_Vertices_of G or v in the_Vertices_of G ) ;

suppose ( V c= the_Vertices_of G & not v in the_Vertices_of G ) ; :: thesis: for v1, e, v2 being object holds
( e Joins v1,v2,G1 iff e Joins v1,v2,G2 )

then G2 is reverseEdgeDirections of G1,G1 .edgesOutOf {v} by Th35;
hence for v1, e, v2 being object holds
( e Joins v1,v2,G1 iff e Joins v1,v2,G2 ) by Th9; :: thesis: verum

end;

suppose ( not V c= the_Vertices_of G or v in the_Vertices_of G ) ; :: thesis: for v1, e, v2 being object holds
( e Joins v1,v2,G1 iff e Joins v1,v2,G2 )

then ( G == G1 & G == G2 ) by Def2, Def3;
then G1 == G2 by GLIB_000:85;
hence for v1, e, v2 being object holds
( e Joins v1,v2,G1 iff e Joins v1,v2,G2 ) by GLIB_000:88; :: thesis: verum

end;

end;