let G, H be finitely_colorable SimpleGraph; :: thesis: ( G c= H implies chromatic# G <= chromatic# H )
assume A: 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;
Aa: G c= H SubgraphInducedBy S by A, Sub0b;
consider C being finite Coloring of H such that
B: card C = chromatic# H by Lchro;
reconsider g = H SubgraphInducedBy S as finitely_colorable SimpleGraph ;
reconsider Cg = C | S as finite Coloring of g by Tsr0;
Ca: Vertices G = Vertices g by Sub0c;
Cb: G c= g

proof

let a be set ; :: 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 SG0;
then A1: ( 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 A1, XBOOLE_0:def 3;

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

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

end;

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

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

end;

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

then a in G ;
hence a in g by Aa; :: 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 A1: x in Cg1 ; :: thesis: x is StableSet of G
reconsider xx = x as Subset of (Vertices G) by A1;
reconsider xxx = x as Subset of (Vertices g) by A1;
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
A2: x <> y and
B2: x in xx and
C2: y in xx ; :: thesis: {x,y} nin G
D2: xxx is stable by A1, LStableSetwise;
assume {x,y} in G ; :: thesis: contradiction
hence contradiction by Cb, A2, B2, C2, D2, Lstable; :: thesis: verum

end;

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

end;

then D: card Cg >= chromatic# G by Lchro;
card C >= card (C | S) by MYCIELSK:8;
hence chromatic# G <= chromatic# H by D, B, XXREAL_0:2; :: thesis: verum