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 )
hereby :: thesis: ( v2 is cut-vertex implies v1 is cut-vertex )
assume A2: v1 is cut-vertex ; :: thesis: v2 is cut-vertex
now :: thesis: for G4 being removeVertex of G2,v2 holds G2 .numComponents() in G4 .numComponents()
let 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;
hence v2 is cut-vertex by GLIB_002:def 10; :: thesis: verum
end;
assume A4: v2 is cut-vertex ; :: thesis: v1 is cut-vertex
now :: thesis: for G3 being removeVertex of G1,v1 holds G1 .numComponents() in G3 .numComponents()
let 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;
hence v1 is cut-vertex by GLIB_002:def 10; :: thesis: verum