let R be non empty with_finite_stability# RelStr ; :: thesis: ( [#] R is Clique of R implies stability# R = 1 )
assume A1: [#] R is Clique of R ; :: thesis: stability# R = 1
A2: stability# R >= 0 + 1 by NAT_1:13;
consider A being finite StableSet of R such that
A3: card A = stability# R by Def6;
assume stability# R <> 1 ; :: thesis: contradiction
then card A > 1 by A2, A3, XXREAL_0:1;
then consider a, b being set such that
A4: a in A and
A5: b in A and
A6: a <> b by NAT_1:59;
thus contradiction by A4, A5, A6, A1, Th15; :: thesis: verum