let H be Subgraph of G; :: thesis: H is finite-ecolorable
consider n being Nat such that
A1: G is n -ecolorable by Def7;
thus H is finite-ecolorable by A1; :: thesis: verum