let R be symmetric with_finite_stability# RelStr ; :: thesis: stability# R = clique# (ComplRelStr R)
set CR = ComplRelStr R;
set k = clique# (ComplRelStr R);
consider A being finite Clique of (ComplRelStr R) such that
A1: card A = clique# (ComplRelStr R) by DILWORTH:def 4;
A is StableSet of R by Th20;
then A2: ex C being finite StableSet of R st card C = clique# (ComplRelStr R) by A1;

now :: thesis: for T being finite StableSet of R holds card T <= clique# (ComplRelStr R)

let T be finite StableSet of R; :: thesis: card T <= clique# (ComplRelStr R)
T is Clique of (ComplRelStr R) by Th21;
hence card T <= clique# (ComplRelStr R) by DILWORTH:def 4; :: thesis: verum

end;

hence stability# R = clique# (ComplRelStr R) by A2, DILWORTH:def 6; :: thesis: verum