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