for G being with_finite_clique# SimpleGraph st 2 <= clique# G holds
for D being finite Clique of (Mycielskian G) holds order D <= clique# G