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
A1: 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)
A4: ( a in C & b in C ) by A2, A3, Lm7;
A5: {a,b} nin Edges G by A4, A1, Def19;
A6: {a,b} in CompleteSGraph (Vertices G) by A4, Th34;
{a,b} in Complement G by A5, A6, XBOOLE_0:def 5;
then {a,b} in (Complement G) SubgraphInducedBy C by A4, Lm10;
hence {a,b} in Edges ((Complement G) SubgraphInducedBy C) by A1, Th12; :: thesis: verum
end;
hence (Complement G) SubgraphInducedBy C is Clique of (Complement G) by Th47; :: thesis: verum