let G2 be _Graph; :: thesis: for v, e, w being object
for G1 being addAdjVertex of G2,v,e,w holds
( G1 is finite-vcolorable iff G2 is finite-vcolorable )
let v, e, w be object ; :: thesis: for G1 being addAdjVertex of G2,v,e,w holds
( G1 is finite-vcolorable iff G2 is finite-vcolorable )
let G1 be addAdjVertex of G2,v,e,w; :: 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 ;

per cases ( not G2 is edgeless or G2 is edgeless ) ;

suppose not G2 is edgeless ; :: thesis: G1 is finite-vcolorable

then G1 is n -vcolorable by A1, Th37;
hence G1 is finite-vcolorable ; :: thesis: verum

end;

suppose G2 is edgeless ; :: thesis: G1 is finite-vcolorable

then G1 is 2 -vcolorable by Th38;
hence G1 is finite-vcolorable ; :: thesis: verum

end;

end;