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