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