let G1 be _Graph; :: thesis: for E being set
for G2 being reverseEdgeDirections of G1,E holds
( G1 is regular iff G2 is regular )
let E be set ; :: thesis: for G2 being reverseEdgeDirections of G1,E holds
( G1 is regular iff G2 is regular )
let G2 be reverseEdgeDirections of G1,E; :: thesis: ( G1 is regular iff G2 is regular )
consider F being PGraphMapping of G1,G2 such that
A1: ( F = id G1 & F is isomorphism ) by GLIBPRE0:77;
thus ( G1 is regular iff G2 is regular ) by A1, Th40; :: thesis: verum