let X be finite set ; :: thesis: chromatic# (CompleteSGraph X) = card X
set n = card X;
set G = CompleteSGraph X;
set D = SmallestPartition X;
A1: card (SmallestPartition X) = card X by TOPGEN_2:12;
A2: Vertices (CompleteSGraph X) = X by Lm1;
reconsider D = SmallestPartition X as a_partition of Vertices (CompleteSGraph X) by Lm1;
A3: D is StableSet-wise

proof

let x be set ; :: according to SCMYCIEL:def 20 :: thesis: ( x in D implies x is StableSet of (CompleteSGraph X) )
assume A4: x in D ; :: thesis: x is StableSet of (CompleteSGraph X)
then reconsider xx = x as Subset of (Vertices (CompleteSGraph X)) ;
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 CompleteSGraph X )
assume that
A5: x <> y and
A6: x in xx and
A7: y in xx ; :: thesis: {x,y} nin CompleteSGraph X
not X is empty by A4;
then D = { {a} where a is Element of X : verum } by EQREL_1:37;
then consider a being Element of X such that
A8: xx = {a} by A4;
( a = x & y = a ) by A8, A6, A7, TARSKI:def 1;
hence {x,y} nin CompleteSGraph X by A5; :: thesis: verum

end;

hence x is StableSet of (CompleteSGraph X) ; :: thesis: verum

end;

for C being finite Coloring of (CompleteSGraph X) holds card X <= card C

proof

let C be finite Coloring of (CompleteSGraph X); :: thesis: card X <= card C
assume A9: card X > card C ; :: thesis: contradiction
then not X is empty ;
then consider p being set , x, y being object such that
A10: p in C and
A11: x in p and
A12: y in p and
A13: x <> y by A9, A2, Th7;
A14: p is StableSet of (CompleteSGraph X) by A10, Def20;
reconsider p = p as Subset of (Vertices (CompleteSGraph X)) by A10;
A15: {x,y} nin CompleteSGraph X by A14, A11, A12, A13, Def19;
p c= X by A2;
hence contradiction by A11, A12, A15, Th34; :: thesis: verum

end;

hence chromatic# (CompleteSGraph X) = card X by A1, A3, Def22; :: thesis: verum