let G1 be _Graph; :: thesis: for G2 being removeLoops 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 removeLoops 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 )

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 )

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 removeLoops 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 )

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 )

hereby :: thesis: ( v2 is cut-vertex implies v1 is cut-vertex )

assume A4:
v2 is cut-vertex
; :: thesis: v1 is cut-vertex assume A2:
v1 is cut-vertex
; :: thesis: v2 is cut-vertex

end;now :: thesis: for G4 being removeVertex of G2,v2 holds G2 .numComponents() in G4 .numComponents()

hence
v2 is cut-vertex
by GLIB_002:def 10; :: thesis: verumlet G4 be removeVertex of G2,v2; :: thesis: G2 .numComponents() in G4 .numComponents()

set G3 = the removeVertex of G1,v1;

G4 is removeLoops of the removeVertex of G1,v1 by A1, Th66;

then A3: the removeVertex of G1,v1 .numComponents() = G4 .numComponents() by Th64;

G1 .numComponents() in the removeVertex of G1,v1 .numComponents() by A2, GLIB_002:def 10;

hence G2 .numComponents() in G4 .numComponents() by A3, Th64; :: thesis: verum

end;set G3 = the removeVertex of G1,v1;

G4 is removeLoops of the removeVertex of G1,v1 by A1, Th66;

then A3: the removeVertex of G1,v1 .numComponents() = G4 .numComponents() by Th64;

G1 .numComponents() in the removeVertex of G1,v1 .numComponents() by A2, GLIB_002:def 10;

hence G2 .numComponents() in G4 .numComponents() by A3, Th64; :: thesis: verum

now :: thesis: for G3 being removeVertex of G1,v1 holds G1 .numComponents() in G3 .numComponents()

hence
v1 is cut-vertex
by GLIB_002:def 10; :: thesis: verumlet G3 be removeVertex of G1,v1; :: thesis: G1 .numComponents() in G3 .numComponents()

set G4 = the removeVertex of G2,v2;

the removeVertex of G2,v2 is removeLoops of G3 by A1, Th66;

then A5: G3 .numComponents() = the removeVertex of G2,v2 .numComponents() by Th64;

G2 .numComponents() in the removeVertex of G2,v2 .numComponents() by A4, GLIB_002:def 10;

hence G1 .numComponents() in G3 .numComponents() by A5, Th64; :: thesis: verum

end;set G4 = the removeVertex of G2,v2;

the removeVertex of G2,v2 is removeLoops of G3 by A1, Th66;

then A5: G3 .numComponents() = the removeVertex of G2,v2 .numComponents() by Th64;

G2 .numComponents() in the removeVertex of G2,v2 .numComponents() by A4, GLIB_002:def 10;

hence G1 .numComponents() in G3 .numComponents() by A5, Th64; :: thesis: verum