let G1 be _Graph; :: thesis: for G2 being SimpleGraph 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 SimpleGraph 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 )
consider H being removeParallelEdges of G1 such that
A1: G2 is removeLoops of H by Th119;
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 A2: v1 = v2 ; :: thesis: ( v1 is cut-vertex iff v2 is cut-vertex )
reconsider v3 = v2 as Vertex of H by A1, GLIB_000:def 33;
( v3 is cut-vertex iff v2 is cut-vertex ) by A1, Th67;
hence ( v1 is cut-vertex iff v2 is cut-vertex ) by A2, Th109; :: thesis: verum