let R be finite RelStr ; :: thesis: for C being Coloring of R holds card C >= clique# R
let C be Coloring of R; :: thesis: card C >= clique# R
assume A: card C < clique# R ; :: thesis: contradiction
consider A being Clique of R such that
B: card A = clique# R by Lheight;
( card (card C) = card C & card (card A) = card A ) ;
then C: card C in card A by A, B, NAT_1:42;
set cR = the carrier of R;

per cases ( R is empty or not R is empty ) ;

suppose S1: R is empty ; :: thesis: contradiction

thus contradiction by A, S1; :: thesis: verum

end;

suppose S1: not R is empty ; :: thesis: contradiction

defpred S₁[ set , set ] means ( $1 in A & $2 in C & $1 in $2 );
P: for x being set st x in A holds
ex y being set st
( y in C & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in A implies ex y being set st
( y in C & S₁[x,y] ) )
assume A1: x in A ; :: thesis: ex y being set st
( y in C & S₁[x,y] )
reconsider x9 = x as Element of R by A1;
not the carrier of R is empty by S1;
then x9 in the carrier of R ;
then x in union C by EQREL_1:def 6;
then consider y being set such that
B1: x in y and
C1: y in C by TARSKI:def 4;
take y ; :: thesis: ( y in C & S₁[x,y] )
thus ( y in C & S₁[x,y] ) by A1, B1, C1; :: thesis: verum

end;

consider f being Function of A,C such that
Q: for x being set st x in A holds
S₁[x,f . x] from FUNCT_2:sch 1(P);
consider x, y being set such that
A1: x in A and
B1: y in A and
C1: x <> y and
D1: f . x = f . y by S1, C, FINSEQ_4:80;
f . x in C by A1, FUNCT_2:7;
then E1: f . x is StableSet of R by LACpart;
( x in f . x & y in f . x ) by D1, A1, B1, Q;
hence contradiction by E1, A1, B1, C1, ACClique; :: thesis: verum

end;

end;