let G1 be _Graph; :: thesis: for G2 being removeDParallelEdges of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v1 is cut-vertex iff v2 is cut-vertex )

let G2 be removeDParallelEdges of G1; :: thesis: for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v1 is cut-vertex iff v2 is cut-vertex )

set G3 = the removeParallelEdges of G2;

let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st v1 = v2 holds

( v1 is cut-vertex iff v2 is cut-vertex )

let v2 be Vertex of G2; :: thesis: ( v1 = v2 implies ( v1 is cut-vertex iff v2 is cut-vertex ) )

assume A1: v1 = v2 ; :: thesis: ( v1 is cut-vertex iff v2 is cut-vertex )

reconsider v3 = v2 as Vertex of the removeParallelEdges of G2 by GLIB_000:def 33;

the removeParallelEdges of G2 is removeParallelEdges of G1 by Th95;

then ( v1 is cut-vertex iff v3 is cut-vertex ) by A1, Th109;

hence ( v1 is cut-vertex iff v2 is cut-vertex ) by Th109; :: thesis: verum

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v1 is cut-vertex iff v2 is cut-vertex )

let G2 be removeDParallelEdges of G1; :: thesis: for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v1 is cut-vertex iff v2 is cut-vertex )

set G3 = the removeParallelEdges of G2;

let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st v1 = v2 holds

( v1 is cut-vertex iff v2 is cut-vertex )

let v2 be Vertex of G2; :: thesis: ( v1 = v2 implies ( v1 is cut-vertex iff v2 is cut-vertex ) )

assume A1: v1 = v2 ; :: thesis: ( v1 is cut-vertex iff v2 is cut-vertex )

reconsider v3 = v2 as Vertex of the removeParallelEdges of G2 by GLIB_000:def 33;

the removeParallelEdges of G2 is removeParallelEdges of G1 by Th95;

then ( v1 is cut-vertex iff v3 is cut-vertex ) by A1, Th109;

hence ( v1 is cut-vertex iff v2 is cut-vertex ) by Th109; :: thesis: verum