theorem Th21: :: DILWORTH:21

for R being with_finite_stability# RelStr st stability# R = 1 holds
[#] R is Clique of R