let E be set ; :: thesis: for G1 being _Graph
for G2 being reverseEdgeDirections of G1,E st G1 is finite-vcolorable holds
G2 is finite-vcolorable
let G1 be _Graph; :: thesis: for G2 being reverseEdgeDirections of G1,E st G1 is finite-vcolorable holds
G2 is finite-vcolorable
let G2 be reverseEdgeDirections of G1,E; :: thesis: ( G1 is finite-vcolorable implies G2 is finite-vcolorable )
assume G1 is finite-vcolorable ; :: thesis: G2 is finite-vcolorable
then consider n being Nat such that
A1: G1 is n -vcolorable ;
G2 is n -vcolorable by A1, Lm2;
hence G2 is finite-vcolorable ; :: thesis: verum