let R be non empty with_finite_clique# RelStr ; :: thesis: ( [#] R is StableSet of R implies clique# R = 1 )
assume A: [#] R is StableSet of R ; :: thesis: clique# R = 1
B: clique# R >= 0 + 1 by NAT_1:13;
consider A being finite Clique of R such that
C: card A = clique# R by Lheight;
assume clique# R <> 1 ; :: thesis: contradiction
then card A > 1 by B, C, XXREAL_0:1;
then consider a, b being set such that
D: a in A and
E: b in A and
F: a <> b by GLIB_002:1;
thus contradiction by D, E, F, A, ACClique; :: thesis: verum