let G, H be finitely_colorable SimpleGraph; :: thesis:
assume A1: G c= H ; :: thesis:
then reconsider S = Vertices G as Subset of (Vertices H) by ZFMISC_1:77;
set g = H SubgraphInducedBy S;
A2: G c= H SubgraphInducedBy S by A1, Th44;
consider C being finite Coloring of H such that
A3: card C = chromatic# H by Def22;
reconsider g = H SubgraphInducedBy S as finitely_colorable SimpleGraph ;
reconsider Cg = C | S as finite Coloring of g by Th67;
A4: Vertices G = Vertices g by Lm9;
A5: G c= g

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in G ; :: thesis:
then a in ({{}} \/ (singletons (Vertices G))) \/ (Edges G) by Th27;
then A6: ( a in {{}} \/ (singletons (Vertices G)) or a in Edges G ) by XBOOLE_0:def 3;

per cases by A6, XBOOLE_0:def 3;

suppose a in {{}} ; :: thesis:

then a = {} by TARSKI:def 1;
hence a in g by Th20; :: thesis:

end;

suppose a in singletons (Vertices G) ; :: thesis:

then a in {{}} \/ (singletons (Vertices g)) by A4, XBOOLE_0:def 3;
then a in ({{}} \/ (singletons (Vertices g))) \/ (Edges g) by XBOOLE_0:def 3;
hence a in g by Th27; :: thesis:

end;

suppose a in Edges G ; :: thesis:

then a in G ;
hence a in g by A2; :: thesis:

end;

end;

end;

reconsider Cg1 = Cg as a_partition of Vertices G ;
Cg1 is StableSet-wise

let x be set ; :: according to SCMYCIEL:def 20 :: thesis:
assume A7: x in Cg1 ; :: thesis:
reconsider xx = x as Subset of (Vertices G) by A7;
reconsider xxx = x as Subset of (Vertices g) by A7;
xx is stable

let x, y be set ; :: according to SCMYCIEL:def 19 :: thesis:
assume that
A8: x <> y and
A9: x in xx and
A10: y in xx ; :: thesis:
A11: xxx is stable by A7, Def20;
assume {x,y} in G ; :: thesis:
hence contradiction by A5, A8, A9, A10, A11; :: thesis:

end;

hence x is StableSet of G ; :: thesis:

end;

then A12: card Cg >= chromatic# G by Def22;
card C >= card (C | S) by MYCIELSK:8;
hence chromatic# G <= chromatic# H by A12, A3, XXREAL_0:2; :: thesis: