set CG = Complement G;
consider A being finite StableSet of G such that
A: for B being finite StableSet of G holds card B <= card A by Lwfstab;
B: Vertices G = Vertices (Complement G) by Compl1;
set C = (Complement G) SubgraphInducedBy A;
reconsider C = (Complement G) SubgraphInducedBy A as finite Clique of (Complement G) by StaCliCompl;
take C ; :: according to SCMYCIEL:def 14 :: thesis: for D being finite Clique of (Complement G) holds order D <= order C
let D be finite Clique of (Complement G); :: thesis: order D <= order C
A1: union D is StableSet of G by CliComplSta;
A = union C by B, Sub0c;
hence order D <= order C by A, A1; :: thesis: verum