let E be set ; :: thesis: for G1 being _Graph
for G2 being reverseEdgeDirections of G1,E holds
( G1 is finite-vcolorable iff G2 is finite-vcolorable )
let G1 be _Graph; :: thesis: for G2 being reverseEdgeDirections of G1,E holds
( G1 is finite-vcolorable iff G2 is finite-vcolorable )
let G2 be reverseEdgeDirections of G1,E; :: thesis: ( G1 is finite-vcolorable iff G2 is finite-vcolorable )
thus ( G1 is finite-vcolorable implies G2 is finite-vcolorable ) by Lm6; :: thesis: ( G2 is finite-vcolorable implies G1 is finite-vcolorable )
G1 is reverseEdgeDirections of G2,E by GLIB_007:3;
hence ( G2 is finite-vcolorable implies G1 is finite-vcolorable ) by Lm6; :: thesis: verum