consider C being Coloring of G such that
A1: C is finite by Def21;
reconsider C = C as finite Coloring of G by A1;
reconsider SX = S /\ (Vertices G) as Subset of (Vertices G) by XBOOLE_1:17;
A2: G SubgraphInducedBy SX = G SubgraphInducedBy S by Th43;
reconsider D = C | SX as Coloring of (G SubgraphInducedBy S) by Th67, A2;
take D ; :: according to SCMYCIEL:def 21 :: thesis: D is finite
thus D is finite ; :: thesis: verum