theorem Th9: :: DILWORTH:9

for R being RelStr
for C being Clique of R
for S being Subset of C holds S is Clique of R