let n be non zero Nat; :: thesis: stability# (CompleteRelStr n) = 1
set R = CompleteRelStr n;
[#] (CompleteRelStr n) is Clique of (CompleteRelStr n) ;
hence stability# (CompleteRelStr n) = 1 by DILWORTH:20; :: thesis: verum