theorem Th6: :: DILWORTH:6

for R being RelStr
for S being Subset of R holds
( S is Clique of R iff for a, b being Element of R st a in S & b in S & a <> b & not a <= b holds
b <= a )