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