let R be finite RelStr ; :: thesis:
let C be Clique-partition of R; :: thesis:
assume A1: card C < stability# R ; :: thesis:
consider A being StableSet of R such that
A2: card A = stability# R by Def6;
( 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 ;

suppose R is empty ; :: thesis:

hence contradiction by A1; :: thesis:

end;

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

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:
assume A6: x in A ; :: thesis:
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:
thus ( y in C & S₁[x,y] ) by A6, A7, A8; :: thesis:

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 Clique of R by Def11;
( 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:

end;

end;