let P be with_finite_clique# with_finite_chromatic# RelStr ; :: thesis: clique# P <= chromatic# P
assume A: clique# P > chromatic# P ; :: thesis: contradiction
consider A being Clique of P such that
B: card A = clique# P by DILWORTH:def 4;
consider C being finite Coloring of P such that
Aa: card C = chromatic# P by Lchro;
( card (card C) = card C & card (card A) = card A ) ;
then C: card C in card A by Aa, A, B, NAT_1:42;
set cP = the carrier of P;

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

suppose P is empty ; :: thesis: contradiction

hence contradiction by A; :: thesis: verum

end;

suppose S1: not P 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] )
then reconsider xp1 = x as Element of P ;
not the carrier of P is empty by S1;
then xp1 in the carrier of P ;
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 P by DILWORTH:def 12;
( x in f . x & y in f . x ) by D1, A1, B1, Q;
hence contradiction by E1, A1, B1, C1, DILWORTH:15; :: thesis: verum

end;

end;