let G2 be _Graph; :: thesis: for E, V 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 .edgesInOut() = v2 .edgesInOut()
let E, V 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 .edgesInOut() = v2 .edgesInOut()
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 .edgesInOut() = v2 .edgesInOut()
let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st v1 = v2 holds
v1 .edgesInOut() = v2 .edgesInOut()
let v2 be Vertex of G2; :: thesis: ( v1 = v2 implies v1 .edgesInOut() = v2 .edgesInOut() )
assume A1: v1 = v2 ; :: thesis: v1 .edgesInOut() = v2 .edgesInOut()
thus v1 .edgesInOut() = G1 .edgesInOut {v1} by GLIB_000:def 40
.= G2 .edgesInOut {v2} by A1, Th12
.= v2 .edgesInOut() by GLIB_000:def 40 ; :: thesis: verum