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 :: thesis: for x, y being Element of (ComplRelStr R) st x in C & y in C & x <> y holds
( not x <= y & not y <= x )
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
A2: y in C and
A3: x <> y ; :: thesis: ( not x <= y & not y <= x )
reconsider a = x, b = y as Element of 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 (ComplRelStr R) by DILWORTH:def 2, NECKLACE:def 8; :: thesis: verum