let G be with_finite_clique# SimpleGraph; :: thesis: clique# G = stability# (Complement G)
set CG = Complement G;
set sCG = stability# (Complement G);
set cG = clique# G;
consider C being finite Clique of G such that
A1: order C = clique# G by Def15;
A2: Vertices G = Vertices (Complement G) by Lm4;
reconsider A = union C as StableSet of (Complement G) by Th72;
A3: card A = clique# G by A1;
now :: thesis: for T being finite StableSet of (Complement G) holds card T <= clique# G
let T be finite StableSet of (Complement G); :: thesis: card T <= clique# G
G SubgraphInducedBy T is Clique of G by Th75;
then order (G SubgraphInducedBy T) <= clique# G by Def15;
hence card T <= clique# G by A2, Lm9; :: thesis: verum
end;
hence clique# G = stability# (Complement G) by A3, Def24; :: thesis: verum