let G be SimpleGraph; :: thesis: for C being StableSet of G holds (Complement G) SubgraphInducedBy C is Clique of (Complement G)
let C be StableSet of G; :: thesis: (Complement G) SubgraphInducedBy C is Clique of (Complement G)
set CG = Complement G;
set CGSC = (Complement G) SubgraphInducedBy C;
set uCGSC = union ((Complement G) SubgraphInducedBy C);

now :: thesis: for a, b being set st a <> b & a in union ((Complement G) SubgraphInducedBy C) & b in union ((Complement G) SubgraphInducedBy C) holds
{a,b} in Edges ((Complement G) SubgraphInducedBy C)

let a, b be set ; :: thesis: ( a <> b & a in union ((Complement G) SubgraphInducedBy C) & b in union ((Complement G) SubgraphInducedBy C) implies {a,b} in Edges ((Complement G) SubgraphInducedBy C) )
assume that
A4: a <> b and
A2: a in union ((Complement G) SubgraphInducedBy C) and
A3: b in union ((Complement G) SubgraphInducedBy C) ; :: thesis: {a,b} in Edges ((Complement G) SubgraphInducedBy C)
B1: ( a in C & b in C ) by A2, A3, Sub1;
D1: {a,b} nin Edges G by B1, A4, Lstable;
E1: {a,b} in CompleteSGraph (Vertices G) by B1, CSG1;
{a,b} in Complement G by D1, E1, XBOOLE_0:def 5;
then {a,b} in (Complement G) SubgraphInducedBy C by B1, Sub6;
hence {a,b} in Edges ((Complement G) SubgraphInducedBy C) by A4, SG4a; :: thesis: verum

end;

hence (Complement G) SubgraphInducedBy C is Clique of (Complement G) by Lclique1; :: thesis: verum