theorem :: ORDERS_1:60

for R being Relation
for x being set holds
( x is_minimal_in R ~ iff x is_maximal_in R )