let X be finite set ; :: thesis: chromatic# (CompleteSGraph X) = card X
set n = card X;
set G = CompleteSGraph X;
set D = SmallestPartition X;
B: card (SmallestPartition X) = card X by TOPGEN_2:12;
D: Vertices (CompleteSGraph X) = X by CSGLem1;
reconsider D = SmallestPartition X as a_partition of Vertices (CompleteSGraph X) by CSGLem1;
Ca: 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 AA: 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
A1: x <> y and
B1: x in xx and
C1: y in xx ; :: thesis: {x,y} nin CompleteSGraph X
not X is empty by AA;
then D = { {a} where a is Element of X : verum } by EQREL_1:37;
then consider a being Element of X such that
D1: xx = {a} and
verum by AA;
( a = x & y = a ) by D1, B1, C1, TARSKI:def 1;
hence {x,y} nin CompleteSGraph X by A1; :: 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 Aa: card X > card C ; :: thesis: contradiction
then not X is empty ;
then consider p, x, y being set such that
A1: p in C and
B1: x in p and
C1: y in p and
D1: x <> y by Aa, D, Part0;
E1: p is StableSet of (CompleteSGraph X) by A1, LStableSetwise;
reconsider p = p as Subset of (Vertices (CompleteSGraph X)) by A1;
F1: {x,y} nin CompleteSGraph X by E1, B1, C1, D1, Lstable;
p c= X by D;
hence contradiction by B1, C1, F1, CSG1; :: thesis: verum

end;

hence chromatic# (CompleteSGraph X) = card X by B, Ca, Lchro; :: thesis: verum