let G, H be finitely_colorable SimpleGraph; :: thesis: ( G c= H implies chromatic# G <= chromatic# H )
assume A1: G c= H ; :: thesis: chromatic# G <= chromatic# H
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

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in G or a in g )
assume a in G ; :: thesis: a in g
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 ( a in {{}} or a in singletons (Vertices G) or a in Edges G ) by A6, XBOOLE_0:def 3;

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

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

end;

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

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: verum

end;

suppose a in Edges G ; :: thesis: a in g

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

end;

end;

end;

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

proof

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

proof

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

end;

hence x is StableSet of G ; :: thesis: verum

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: verum