let R be RelStr ; :: thesis: for C being StableSet of (ComplRelStr R) holds C is Clique of R
let C be StableSet of (ComplRelStr R); :: thesis: C is Clique of R
A0: the carrier of R = the carrier of (ComplRelStr R) by NECKLACE:def 9;

now

let a, b be Element of R; :: thesis: ( a in C & b in C & a <> b & not a <= b implies b <= a )
assume that
A: a in C and
B: b in C and
C: a <> b ; :: thesis: ( a <= b or b <= a )
reconsider ap1 = a, bp1 = b as Element of (ComplRelStr R) by NECKLACE:def 9;
( not ap1 <= bp1 & not bp1 <= ap1 ) by A, B, C, DILWORTH:def 2;
hence ( a <= b or b <= a ) by C, A, A0, DCompl1; :: thesis: verum

end;

hence C is Clique of R by NECKLACE:def 9, DILWORTH:6; :: thesis: verum