set CG = Complement G;
consider A being finite Clique of G such that
A1: for B being finite Clique of G holds order B <= order A by Def14;
A2: Vertices G = Vertices (Complement G) by Lm4;
set C = union A;
reconsider C = union A as finite StableSet of (Complement G) by Th72;
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
A3: G SubgraphInducedBy D is finite Clique of G by Th75;
order (G SubgraphInducedBy D) <= order A by A3, A1;
hence card D <= card C by A2, Lm9; :: thesis: verum