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

now :: thesis: for x, y being Element of R st x in C & y in C & x <> y holds
( not x <= y & not y <= x )

let x, y be Element of R; :: thesis: ( x in C & y in C & x <> y implies ( not x <= y & not y <= x ) )
assume that
A1: x in C and
A2: y in C and
A3: x <> y ; :: thesis: ( not x <= y & not y <= x )
reconsider a = x, b = y as Element of (ComplRelStr R) by NECKLACE:def 8;
( a <= b or b <= a ) by A1, A2, A3, DILWORTH:6;
then ( a <= b & b <= a ) by Th6;
hence ( not x <= y & not y <= x ) by Th17; :: thesis: verum

end;

hence C is StableSet of R by DILWORTH:def 2, NECKLACE:def 8; :: thesis: verum