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

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

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

end;

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