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 A1: clique# G = 0 ; :: thesis: for D being finite Clique of (Mycielskian G) holds order D <= 1
set uG = union G;
A2: Vertices G = {} by A1, Th54;
A3: G is void by A2, Th28;
A4: union (Mycielskian G) = union {{},{(union G)}} by A3, Th88
.= {} \/ {(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 A4, ZFMISC_1:77;
then Segm (card (Vertices D)) c= Segm (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