let G be with_finite_clique# SimpleGraph; :: thesis: ( 2 <= clique# G implies clique# (Mycielskian G) = clique# G )
assume that
A1: 2 <= clique# G and
A2: clique# (Mycielskian G) <> clique# G ; :: thesis: contradiction
set MG = Mycielskian G;
consider D being finite Clique of (Mycielskian G) such that
A3: order D = clique# (Mycielskian G) by Def15;
clique# G <= clique# (Mycielskian G) by Th84, Th58;
then clique# G < clique# (Mycielskian G) by A2, XXREAL_0:1;
hence contradiction by A1, A3, Th109; :: thesis: verum