let G1 be _Graph; :: thesis: for E being set
for G2 being reverseEdgeDirections of G1,E holds G2 is G1 -isomorphic
let E be set ; :: thesis: for G2 being reverseEdgeDirections of G1,E holds G2 is G1 -isomorphic
let G2 be reverseEdgeDirections of G1,E; :: thesis: G2 is G1 -isomorphic
consider F being PGraphMapping of G1,G2 such that
A1: ( F = id G1 & F is isomorphism ) by Th83;
thus G2 is G1 -isomorphic by A1, GLIB_010:def 23; :: thesis: verum