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