let G1 be _Graph; :: thesis: for G2 being removeDParallelEdges of G1
for v1, w1 being Vertex of G1
for v2, w2 being Vertex of G2 st v1 = v2 & w1 = w2 holds
( v1,w1 are_adjacent iff v2,w2 are_adjacent )
let G2 be removeDParallelEdges of G1; :: thesis: for v1, w1 being Vertex of G1
for v2, w2 being Vertex of G2 st v1 = v2 & w1 = w2 holds
( v1,w1 are_adjacent iff v2,w2 are_adjacent )
let v1, w1 be Vertex of G1; :: thesis: for v2, w2 being Vertex of G2 st v1 = v2 & w1 = w2 holds
( v1,w1 are_adjacent iff v2,w2 are_adjacent )
let v2, w2 be Vertex of G2; :: thesis: ( v1 = v2 & w1 = w2 implies ( v1,w1 are_adjacent iff v2,w2 are_adjacent ) )
assume A1: ( v1 = v2 & w1 = w2 ) ; :: thesis: ( v1,w1 are_adjacent iff v2,w2 are_adjacent )

hereby :: thesis: ( v2,w2 are_adjacent implies v1,w1 are_adjacent )

assume v1,w1 are_adjacent ; :: thesis: v2,w2 are_adjacent
then w1 in v1 .allNeighbors() by Th42;
then w2 in v2 .allNeighbors() by A1, GLIBPRE0:65;
hence v2,w2 are_adjacent by Th42; :: thesis: verum

end;

assume v2,w2 are_adjacent ; :: thesis: v1,w1 are_adjacent
then w2 in v2 .allNeighbors() by Th42;
then w1 in v1 .allNeighbors() by A1, GLIBPRE0:65;
hence v1,w1 are_adjacent by Th42; :: thesis: verum