for L being non empty transitive antisymmetric RelStr
for x being Element of L
for a, N being set st a is_minimal_wrt ( the InternalRel of L -Seg x) /\ N, the InternalRel of L holds
a is_minimal_wrt N, the InternalRel of L