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;
A: Vertices (G SubgraphInducedBy S) = S /\ (Vertices G) by Sub5
.= S by XBOOLE_1:28 ;
reconsider CS = C | S as a_partition of Vertices (G SubgraphInducedBy S) by A;
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 A1: x in CS ; :: thesis: x is StableSet of (G SubgraphInducedBy S)
reconsider xx = x as Subset of (Vertices (G SubgraphInducedBy S)) by A1;
consider z being Element of C such that
B1: xx = z /\ S and
z meets S 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 SubgraphInducedBy S )
assume that
A2: x <> y and
B2: x in xx and
C2: y in xx ; :: thesis: {x,y} nin G SubgraphInducedBy S
assume D2a: {x,y} in G SubgraphInducedBy S ; :: thesis: contradiction
E2: x in z by B1, B2, XBOOLE_0:def 4;
F2: y in z by C2, B1, XBOOLE_0:def 4;
z is StableSet of G by B1, B2, LStableSetwise;
hence contradiction by D2a, A2, E2, F2, Lstable; :: 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