let V be set ; :: thesis: for G2 being _Graph
for G1 being addVertices of G2,V holds
( G1 is finite-ecolorable iff G2 is finite-ecolorable )
let G2 be _Graph; :: thesis: for G1 being addVertices of G2,V holds
( G1 is finite-ecolorable iff G2 is finite-ecolorable )
let G1 be addVertices of G2,V; :: thesis: ( G1 is finite-ecolorable iff G2 is finite-ecolorable )

hereby :: thesis: ( G2 is finite-ecolorable implies G1 is finite-ecolorable )

assume G1 is finite-ecolorable ; :: thesis: G2 is finite-ecolorable
then consider n being Nat such that
A1: G1 is n -ecolorable ;
G2 is n -ecolorable by A1, Th105;
hence G2 is finite-ecolorable ; :: thesis: verum

end;

assume G2 is finite-ecolorable ; :: thesis: G1 is finite-ecolorable
then consider n being Nat such that
A2: G2 is n -ecolorable ;
thus G1 is finite-ecolorable by A2; :: thesis: verum