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 ) & ( v2 is isolated implies v1 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) & ( v2 is endvertex implies v1 is endvertex ) & ( v1 is cut-vertex implies v2 is cut-vertex ) & ( v2 is cut-vertex implies v1 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 ) & ( v2 is isolated implies v1 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) & ( v2 is endvertex implies v1 is endvertex ) & ( v1 is cut-vertex implies v2 is cut-vertex ) & ( v2 is cut-vertex implies v1 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 ) & ( v2 is isolated implies v1 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) & ( v2 is endvertex implies v1 is endvertex ) & ( v1 is cut-vertex implies v2 is cut-vertex ) & ( v2 is cut-vertex implies v1 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 ) & ( v2 is isolated implies v1 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) & ( v2 is endvertex implies v1 is endvertex ) & ( v1 is cut-vertex implies v2 is cut-vertex ) & ( v2 is cut-vertex implies v1 is cut-vertex ) )
let v2 be Vertex of G2; :: thesis: ( v1 = v2 implies ( ( v1 is isolated implies v2 is isolated ) & ( v2 is isolated implies v1 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) & ( v2 is endvertex implies v1 is endvertex ) & ( v1 is cut-vertex implies v2 is cut-vertex ) & ( v2 is cut-vertex implies v1 is cut-vertex ) ) )
assume A1: v1 = v2 ; :: thesis: ( ( v1 is isolated implies v2 is isolated ) & ( v2 is isolated implies v1 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) & ( v2 is endvertex implies v1 is endvertex ) & ( v1 is cut-vertex implies v2 is cut-vertex ) & ( v2 is cut-vertex implies v1 is cut-vertex ) )
G2 is reverseEdgeDirections of G1,E by Th3;
hence ( ( v1 is isolated implies v2 is isolated ) & ( v2 is isolated implies v1 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) & ( v2 is endvertex implies v1 is endvertex ) & ( v1 is cut-vertex implies v2 is cut-vertex ) & ( v2 is cut-vertex implies v1 is cut-vertex ) ) by A1, Lm5; :: thesis: verum