let R be with_finite_clique# RelStr ; :: thesis: ( clique# R = 1 implies [#] R is StableSet of R )
assume A: clique# R = 1 ; :: thesis: [#] R is StableSet of R
set cR = the carrier of R;
D: not R is empty by A;

now

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

end;

hence [#] R is StableSet of R by LAChain; :: thesis: verum