let R be with_finite_stability# RelStr ; :: thesis: ( stability# R = 1 implies [#] R is Clique of R )
assume A: stability# R = 1 ; :: thesis: [#] R is Clique of R
set cR = the carrier of R;

now

let a, b be Element of R; :: thesis: ( a in the carrier of R & b in the carrier of R & a <> b & not a <= b implies b <= a )
assume that
A1: a in the carrier of R and
b in the carrier of R and
C1: a <> b ; :: thesis: ( a <= b or b <= a )
E1: not R is empty by A1;
assume ( not a <= b & not b <= a ) ; :: thesis: contradiction
then D1: {a,b} is StableSet of R by E1, AChain36b;
card {a,b} = 2 by C1, CARD_2:76;
hence contradiction by A, Lwidth, D1; :: thesis: verum

end;

hence [#] R is Clique of R by DClique; :: thesis: verum