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 A1: card C < clique# R ; :: thesis: contradiction
consider A being Clique of R such that
A2: card A = clique# R by Def4;
( card (Segm (card C)) = card C & card (Segm (card A)) = card A ) ;
then A3: card C in card A by A1, A2, NAT_1:41;
set cR = the carrier of R;

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

suppose R is empty ; :: thesis: contradiction

hence contradiction by A1; :: thesis: verum

end;

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

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

proof

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

end;

consider f being Function of A,C such that
A9: for x being object st x in A holds
S₁[x,f . x] from FUNCT_2:sch 1(A5);
consider x, y being object such that
A10: x in A and
A11: y in A and
A12: x <> y and
A13: f . x = f . y by A4, A3, FINSEQ_4:65;
f . x in C by A10, FUNCT_2:5;
then A14: f . x is StableSet of R by Def12;
( S₁[x,f . x] & S₁[y,f . y] ) by A10, A11, A9;
then ( x in f . x & y in f . x ) by A13;
hence contradiction by A14, A10, A11, A12, Th15; :: thesis: verum

end;

end;