let G be SimpleGraph; :: thesis: for C being StableSet of (Complement G) holds G SubgraphInducedBy C is Clique of G
let C be StableSet of (Complement G); :: thesis: G SubgraphInducedBy C is Clique of G
(Complement (Complement G)) SubgraphInducedBy C is Clique of (Complement (Complement G)) by Th74;
hence G SubgraphInducedBy C is Clique of G ; :: thesis: verum