for R being transitive antisymmetric RelStr
for A being StableSet of R
for z being set st z in Upper A & z in Lower A holds
z in A