for R being non empty transitive antisymmetric with_finite_clique# RelStr
for x being Element of R ex y being Element of R st
( y is_minimal_in [#] R & ( y = x or y < x ) )