let R be symmetric RelStr ; :: thesis: for C being Clique of R holds C is StableSet of (ComplRelStr R)
let C be Clique of R; :: thesis: C is StableSet of (ComplRelStr R)

now

let x, y be Element of (ComplRelStr R); :: thesis: ( x in C & y in C & x <> y implies ( not x <= y & not y <= x ) )
assume that
A1: x in C and
B1: y in C and
C1: x <> y ; :: thesis: ( not x <= y & not y <= x )
reconsider a = x, b = y as Element of R by NECKLACE:def 9;
( a <= b or b <= a ) by A1, B1, C1, DILWORTH:6;
then ( a <= b & b <= a ) by Sym0;
hence ( not x <= y & not y <= x ) by DCompl; :: thesis: verum

end;

hence C is StableSet of (ComplRelStr R) by NECKLACE:def 9, DILWORTH:def 2; :: thesis: verum