for R being with_finite_stability# RelStr
for A being StableSet of R
for C being Clique-partition of R st card C = card A holds
ex f being Function of A,C st
( f is bijective & ( for x being set st x in A holds
x in f . x ) )