let G be with_finite_clique# SimpleGraph; :: thesis: ( 2 <= clique# G implies clique# (Mycielskian G) = clique# G )
assume that
A: 2 <= clique# G and
B: clique# (Mycielskian G) <> clique# G ; :: thesis: contradiction
set MG = Mycielskian G;
consider D being finite Clique of (Mycielskian G) such that
D: order D = clique# (Mycielskian G) by Lcliqueno;
clique# G <= clique# (Mycielskian G) by M0, CliqueSubno0;
then clique# G < clique# (Mycielskian G) by B, XXREAL_0:1;
hence contradiction by A, D, MClique2; :: thesis: verum