let G be SimpleGraph; :: thesis: for C being Clique of G holds Vertices C is StableSet of (Complement G)
let C be Clique of G; :: thesis: Vertices C is StableSet of (Complement G)
set CG = Complement G;
A: Vertices G = Vertices (Complement G) by Compl1;
reconsider uC = union C as Subset of (Vertices (Complement G)) by A, ZFMISC_1:77;

now :: thesis: for x, y being set st x <> y & x in uC & y in uC holds
{x,y} nin Complement G

let x, y be set ; :: thesis: ( x <> y & x in uC & y in uC implies {x,y} nin Complement G )
assume that
A3: x <> y and
A1: x in uC and
A2: y in uC ; :: thesis: {x,y} nin Complement G
{x,y} in C by A1, A2, Clique2a;
then {x,y} in Edges G by A3, SG4a;
hence {x,y} nin Complement G by XBOOLE_0:def 5; :: thesis: verum

end;

hence union C is StableSet of (Complement G) by Lstable; :: thesis: verum