let G be with_finite_clique# SimpleGraph; :: thesis: ( clique# G = 0 implies for D being finite Clique of (Mycielskian G) holds order D <= 1 )
assume A: clique# G = 0 ; :: thesis: for D being finite Clique of (Mycielskian G) holds order D <= 1
set uG = union G;
B: Vertices G = {} by A, Cno0;
C: G is void by B, VoidGV;
D: union (Mycielskian G) = union {{},{(union G)}} by C, MGvoid
.= {} \/ {(union G)} by ZFMISC_1:75
.= {(union G)} ;
let D be finite Clique of (Mycielskian G); :: thesis: order D <= 1
Vertices D c= {(union G)} by D, ZFMISC_1:77;
then card (Vertices D) c= card {(union G)} by CARD_1:11;
then card (Vertices D) <= card {(union G)} by NAT_1:39;
hence order D <= 1 by CARD_1:30; :: thesis: verum