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;
A1: Vertices G = Vertices (Complement G) by Lm4;
reconsider uC = union C as Subset of (Vertices (Complement G)) by A1, 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
A2: x <> y and
A3: x in uC and
A4: y in uC ; :: thesis: {x,y} nin Complement G
{x,y} in C by A3, A4, Th53;
then {x,y} in Edges G by A2, Th12;
hence {x,y} nin Complement G by XBOOLE_0:def 5; :: thesis: verum

end;

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