for G being with_finite_clique# SimpleGraph st clique# G = 0 holds
Vertices G = {}