for R being non empty transitive antisymmetric RelStr
for X being finite Subset of R st X <> {} holds
ex x being Element of R st
( x in X & x is_minimal_wrt X, the InternalRel of R )