let R be non empty with_finite_stability# RelStr ; :: thesis: ( [#] R is Clique of R implies stability# R = 1 )
assume A: [#] R is Clique of R ; :: thesis: stability# R = 1
B: stability# R >= 0 + 1 by NAT_1:13;
consider A being finite StableSet of R such that
C: card A = stability# R by Lwidth;
assume stability# R <> 1 ; :: thesis: contradiction
then card A > 1 by B, C, XXREAL_0:1;
then consider a, b being set such that
D: a in A and
E: b in A and
F: a <> b by GLIB_002:1;
thus contradiction by D, E, F, A, ACClique; :: thesis: verum