theorem Th42: :: DILWORTH:42

for R being with_finite_clique# RelStr
for S being Subset of R holds clique# (subrelstr S) <= clique# R