let H be Subgraph of G; :: thesis: H is finite-tcolorable
consider n being Nat such that
A1: G is n -tcolorable by Def12;
H is n -tcolorable by A1, Th166;
hence H is finite-tcolorable ; :: thesis: verum