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