set MG = Mycielskian G;
set uG = union G;

per cases by NAT_1:25;

suppose A1: clique# G = 0 ; :: thesis:

then union G = {} by Th54;
then {} in union (Mycielskian G) by Th87;
then consider C being finite Clique of (Mycielskian G) such that
A2: Vertices C = {{}} by Th52;
take C ; :: according to SCMYCIEL:def 14 :: thesis:
order C = 1 by A2, CARD_1:30;
hence for D being finite Clique of (Mycielskian G) holds order D <= order C by A1, Th106; :: thesis:

end;

suppose A3: clique# G = 1 ; :: thesis:

then consider C being finite Clique of G such that
A4: order C = 1 by Def15;
A5: union C c= union G by ZFMISC_1:77;
Vertices C <> {} by A4;
then consider v being object such that
A6: v in Vertices C by XBOOLE_0:def 1;
A7: [v,(union G)] in union (Mycielskian G) by A6, A5, Th85;
A8: union G in union (Mycielskian G) by Th87;
A9: {[v,(union G)],(union G)} in Mycielskian G by A6, A5, Th96;
reconsider CC = {{},{[v,(union G)]},{(union G)},{[v,(union G)],(union G)}} as finite Clique of (Mycielskian G) by A7, A8, A9, Th51;
A10: CC = CompleteSGraph {[v,(union G)],(union G)} by Th37;
A11: Vertices CC = {[v,(union G)],(union G)} by A10, Lm1;
take CC ; :: according to SCMYCIEL:def 14 :: thesis:
order CC = 2 by A11, Th2, CARD_2:57;
hence for D being finite Clique of (Mycielskian G) holds order D <= order CC by A3, Th108; :: thesis:

end;

suppose clique# G > 1 ; :: thesis:

then A12: clique# G >= 1 + 1 by NAT_1:13;
consider C being finite Clique of G such that
A13: order C = clique# G by Def15;
G c= Mycielskian G by Th84;
then reconsider CC = C as finite Clique of (Mycielskian G) by XBOOLE_1:1;
take CC ; :: according to SCMYCIEL:def 14 :: thesis:
thus for D being finite Clique of (Mycielskian G) holds order D <= order CC by A13, A12, Th109; :: thesis:

end;

end;