let R be RelStr ; :: thesis: for C being StableSet of R holds C is Clique of (ComplRelStr R)
let C be StableSet of R; :: thesis: C is Clique of (ComplRelStr R)
set CR = ComplRelStr R;
A1: C is Subset of (ComplRelStr R) by NECKLACE:def 8;

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

let a, b be Element of (ComplRelStr R); :: thesis: ( a in C & b in C & a <> b & not a <= b implies b <= a )
assume that
A2: a in C and
A3: b in C and
A4: a <> b ; :: thesis: ( a <= b or b <= a )
reconsider ap1 = a, bp1 = b as Element of R by NECKLACE:def 8;
( not ap1 <= bp1 & not bp1 <= ap1 ) by A2, A3, A4, DILWORTH:def 2;
hence ( a <= b or b <= a ) by A2, A4, Th18; :: thesis: verum

end;

hence C is Clique of (ComplRelStr R) by A1, DILWORTH:6; :: thesis: verum