let G1 be _Graph; :: thesis: for G2 being removeDParallelEdges of G1 holds
( G1 is finite-vcolorable iff G2 is finite-vcolorable )
let G2 be removeDParallelEdges of G1; :: thesis: ( G1 is finite-vcolorable iff G2 is finite-vcolorable )
thus ( G1 is finite-vcolorable implies G2 is finite-vcolorable ) ; :: thesis: ( G2 is finite-vcolorable implies G1 is finite-vcolorable )
assume G2 is finite-vcolorable ; :: thesis: G1 is finite-vcolorable
then consider n being Nat such that
A1: G2 is n -vcolorable ;
G1 is n -vcolorable by A1, Th41;
hence G1 is finite-vcolorable ; :: thesis: verum