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