let P be with_finite_clique# with_finite_chromatic# RelStr ; :: thesis: clique# P <= chromatic# P
assume A1: clique# P > chromatic# P ; :: thesis: contradiction
consider A being Clique of P such that
A2: card A = clique# P by DILWORTH:def 4;
consider C being finite Coloring of P such that
A3: card C = chromatic# P by Def3;
( card (Segm (card C)) = card C & card (Segm (card A)) = card A ) ;
then A4: card C in card A by A3, A1, A2, NAT_1:41;
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 A1; :: thesis: verum
end;
suppose A5: not P is empty ; :: thesis: contradiction
defpred S2[ object , object ] means ex D2 being set st
( D2 = $2 & $1 in A & $2 in C & $1 in D2 );
A6: for x being object st x in A holds
ex y being object st
( y in C & S2[x,y] )
proof
let x be object ; :: thesis: ( x in A implies ex y being object st
( y in C & S2[x,y] ) )
assume A7: x in A ; :: thesis: ex y being object st
( y in C & S2[x,y] )
then reconsider xp1 = x as Element of P ;
not the carrier of P is empty by A5;
then xp1 in the carrier of P ;
then x in union C by EQREL_1:def 4;
then consider y being set such that
A8: x in y and
A9: y in C by TARSKI:def 4;
take y ; :: thesis: ( y in C & S2[x,y] )
thus ( y in C & S2[x,y] ) by A7, A8, A9; :: thesis: verum
end;
consider f being Function of A,C such that
A10: for x being object st x in A holds
S2[x,f . x] from FUNCT_2:sch 1(A6);
consider x, y being object such that
A11: x in A and
A12: y in A and
A13: x <> y and
A14: f . x = f . y by A5, A4, FINSEQ_4:65;
f . x in C by A11, FUNCT_2:5;
then A15: f . x is StableSet of P by DILWORTH:def 12;
( S2[x,f . x] & S2[y,f . y] ) by A11, A12, A10;
then ( x in f . x & y in f . x ) by A14;
hence contradiction by A15, A11, A12, A13, DILWORTH:15; :: thesis: verum
end;
end;