let R be non empty with_finite_clique# RelStr ; :: thesis: ( [#] R is StableSet of R implies clique# R = 1 )
assume A1: [#] R is StableSet of R ; :: thesis: clique# R = 1
A2: clique# R >= 0 + 1 by NAT_1:13;
consider A being finite Clique of R such that
A3: card A = clique# R by Def4;
assume clique# R <> 1 ; :: thesis: contradiction
then card A > 1 by A2, A3, XXREAL_0:1;
then consider a, b being set such that
A4: a in A and
A5: b in A and
A6: a <> b by NAT_1:59;
thus contradiction by A4, A5, A6, A1, Th15; :: thesis: verum