let R be with_finite_clique# SimpleGraph; :: thesis: ( clique# R = 1 implies Vertices R is StableSet of R )
assume A1: clique# R = 1 ; :: thesis: Vertices R is StableSet of R
set cR = Vertices R;
A2: Vertices R c= Vertices R ;

now :: thesis: for a, b being set st a <> b & a in Vertices R & b in Vertices R holds
not {a,b} in R

let a, b be set ; :: thesis: ( a <> b & a in Vertices R & b in Vertices R implies not {a,b} in R )
assume A3: ( a <> b & a in Vertices R & b in Vertices R ) ; :: thesis: not {a,b} in R
A4: {a,b} c= Vertices R by A3, ZFMISC_1:32;
assume {a,b} in R ; :: thesis: contradiction
then reconsider H = R SubgraphInducedBy {a,b} as finite Clique of R by Th56;
Vertices H = {a,b} by A4, Lm9;
then order H = 2 by A3, CARD_2:57;
hence contradiction by A1, Def15; :: thesis: verum

end;

hence Vertices R is StableSet of R by A2, Def19; :: thesis: verum