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
A: order C = clique# G by Lcliqueno;
B: Vertices G = Vertices (Complement G) by Compl1;
reconsider A = union C as StableSet of (Complement G) by CliStaCompl;
X: card A = clique# G by A;

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 StaComplCli;
then order (G SubgraphInducedBy T) <= clique# G by Lcliqueno;
hence card T <= clique# G by B, Sub0c; :: thesis: verum

end;

hence clique# G = stability# (Complement G) by X, Lstabno; :: thesis: verum