let R be with_finite_stability# with_finite_cliquecover# RelStr ; :: thesis: stability# R <= cliquecover# R
assume A1: stability# R > cliquecover# R ; :: thesis: contradiction
consider A being StableSet of R such that
A2: card A = stability# R by DILWORTH:def 6;
consider C being finite Clique-partition of R such that
A3: card C = cliquecover# R by Def5;
( 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 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 A5: not R 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] )
reconsider xp1 = x as Element of R by A7;
not the carrier of R is empty by A5;
then xp1 in the carrier of R ;
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 Clique of R by DILWORTH:def 11;
( 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;