theorem :: ORDERS_1:53

for R being Relation
for x being set st x is_inferior_of R & R is antisymmetric holds
x is_minimal_in R