for G being with_finite_clique# SimpleGraph st Edges G <> {} holds
clique# G >= 2