let G be SimpleGraph; :: thesis: for C being Coloring of G
for S being Subset of (Vertices G) holds C | S is Coloring of (G SubgraphInducedBy S)
let C be Coloring of G; :: thesis: for S being Subset of (Vertices G) holds C | S is Coloring of (G SubgraphInducedBy S)
let S be Subset of (Vertices G); :: thesis: C | S is Coloring of (G SubgraphInducedBy S)
set g = G SubgraphInducedBy S;
A1: Vertices (G SubgraphInducedBy S) = S /\ (Vertices G) by Th45
.= S by XBOOLE_1:28 ;
reconsider CS = C | S as a_partition of Vertices (G SubgraphInducedBy S) by A1;
CS is StableSet-wise

proof

let x be set ; :: according to SCMYCIEL:def 20 :: thesis: ( x in CS implies x is StableSet of (G SubgraphInducedBy S) )
assume A2: x in CS ; :: thesis: x is StableSet of (G SubgraphInducedBy S)
reconsider xx = x as Subset of (Vertices (G SubgraphInducedBy S)) by A2;
consider z being Element of C such that
A3: xx = z /\ S and
z meets S by A2;
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 SubgraphInducedBy S )
assume that
A4: x <> y and
A5: x in xx and
A6: y in xx ; :: thesis: {x,y} nin G SubgraphInducedBy S
assume A7: {x,y} in G SubgraphInducedBy S ; :: thesis: contradiction
A8: x in z by A3, A5, XBOOLE_0:def 4;
A9: y in z by A6, A3, XBOOLE_0:def 4;
z is StableSet of G by A3, A5, Def20;
hence contradiction by A7, A4, A8, A9, Def19; :: thesis: verum

end;

hence x is StableSet of (G SubgraphInducedBy S) ; :: thesis: verum

end;

hence C | S is Coloring of (G SubgraphInducedBy S) ; :: thesis: verum