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
A2: a <> b and
A3: ( 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 A2, Th12;
then A4: {a,b} is StableSet of R by A3, Th62;
card {a,b} = 2 by A2, CARD_2:57;
hence contradiction by A1, A4, Def24; :: thesis: verum
end;
hence R is clique by Th47; :: thesis: verum