let R be with_finite_stability# SimpleGraph; :: thesis: ( stability# R = 1 implies R is clique )
assume A1: stability# R = 1 ; :: thesis: R is clique
set cR = Vertices R;

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

let a, b be set ; :: thesis: ( a <> b & a in Vertices R & b in Vertices R implies not {a,b} nin Edges R )
assume that
A3: a <> b and
A2: ( a in Vertices R & b in Vertices R ) ; :: thesis: not {a,b} nin Edges R
assume {a,b} nin Edges R ; :: thesis: contradiction
then {a,b} nin R by A3, SG4a;
then A5: {a,b} is StableSet of R by A2, Th14;
card {a,b} = 2 by A3, CARD_2:57;
hence contradiction by A1, A5, Lstabno; :: thesis: verum

end;

hence R is clique by Lclique1; :: thesis: verum