theorem Th59: :: ORDERS_1:59

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