for G, H being with_finite_clique# SimpleGraph st G c= H holds
clique# G <= clique# H