let R be with_finite_stability# RelStr ; :: thesis: ( stability# R = 1 implies [#] R is Clique of R )
assume A1: stability# R = 1 ; :: thesis: [#] R is Clique of R
set cR = the carrier of R;
now :: thesis: for a, b being Element of R st a in the carrier of R & b in the carrier of R & a <> b & not a <= b holds
b <= a
let a, b be Element of R; :: thesis: ( a in the carrier of R & b in the carrier of R & a <> b & not a <= b implies b <= a )
assume that
A2: a in the carrier of R and
b in the carrier of R and
A3: a <> b ; :: thesis: ( a <= b or b <= a )
A4: not R is empty by A2;
assume ( not a <= b & not b <= a ) ; :: thesis: contradiction
then A5: {a,b} is StableSet of R by A4, Th14;
card {a,b} = 2 by A3, CARD_2:57;
hence contradiction by A1, Def6, A5; :: thesis: verum
end;
hence [#] R is Clique of R by Th6; :: thesis: verum