let G2 be _Graph; :: thesis: for E being set
for G1 being reverseEdgeDirections of G2,E
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( ( v1 is isolated implies v2 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) & ( v1 is cut-vertex implies v2 is cut-vertex ) )
let E be set ; :: thesis: for G1 being reverseEdgeDirections of G2,E
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( ( v1 is isolated implies v2 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) & ( v1 is cut-vertex implies v2 is cut-vertex ) )
let G1 be reverseEdgeDirections of G2,E; :: thesis: for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( ( v1 is isolated implies v2 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) & ( v1 is cut-vertex implies v2 is cut-vertex ) )
let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st v1 = v2 holds
( ( v1 is isolated implies v2 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) & ( v1 is cut-vertex implies v2 is cut-vertex ) )
let v2 be Vertex of G2; :: thesis: ( v1 = v2 implies ( ( v1 is isolated implies v2 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) & ( v1 is cut-vertex implies v2 is cut-vertex ) ) )
assume A1: v1 = v2 ; :: thesis: ( ( v1 is isolated implies v2 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) & ( v1 is cut-vertex implies v2 is cut-vertex ) )

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

assume v1 is isolated ; :: thesis: v2 is isolated
then v1 .edgesInOut() = {} by GLIB_000:def 49;
then v2 .edgesInOut() = {} by A1, Th13;
hence v2 is isolated by GLIB_000:def 49; :: thesis: verum

end;

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

assume v1 is endvertex ; :: thesis: v2 is endvertex
then consider e being object such that
A2: ( v1 .edgesInOut() = {e} & not e Joins v1,v1,G1 ) by GLIB_000:def 51;
A3: not e Joins v2,v2,G2 by A1, A2, Th9;
v2 .edgesInOut() = {e} by A1, A2, Th13;
hence v2 is endvertex by A3, GLIB_000:def 51; :: thesis: verum

end;

assume A4: v1 is cut-vertex ; :: thesis: v2 is cut-vertex
for G4 being removeVertex of G2,v2 holds G2 .numComponents() in G4 .numComponents()

proof

let G4 be removeVertex of G2,v2; :: thesis: G2 .numComponents() in G4 .numComponents()
set G3 = the removeVertex of G1,v1;
G4 is reverseEdgeDirections of the removeVertex of G1,v1,E \ (G1 .edgesInOut {v2}) by A1, Th22;
then A5: G4 .numComponents() = the removeVertex of G1,v1 .numComponents() by Th21;
G1 .numComponents() in the removeVertex of G1,v1 .numComponents() by A4, GLIB_002:def 10;
hence G2 .numComponents() in G4 .numComponents() by A5, Th21; :: thesis: verum

end;

hence v2 is cut-vertex by GLIB_002:def 10; :: thesis: verum