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