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